rbarreiro/idrisjs

Js libraries for idris

idrisjs's Issues

Examples fail with missing continuation

With Idris 1.0, all the examples fail as soon as getInput returns, because its continuation is missing from the emitted Javascript. For example, with ex01, as soon as I enter any text in the textbox, I get this:

ex0.html:447 Uncaught ReferenceError: _idris__123_APPLY0_125_ is not defined
    at Object.read (ex0.html:447)
    at processEvent (ex0.html:26)
    at HTMLInputElement.<anonymous> (ex0.html:39)
(anonymous) @ ex0.html:447
processEvent @ ex0.html:26
(anonymous) @ ex0.html:39

Purely UI callbacks that don't generate events

Sometimes you need to install listeners just to change the internal state of UI components.

For example, in this code I'd like to make an input box that selects its whole contents on focus, because the user will always want to replace the contents wholesale. According to this StackOverflow answer this requres installing onfocus and onmouseup handlers; however, these handlers shouldn't generate an event as far as idrisjs is concerned (i.e. there's no value to return from getInput).

Can we add this kind of "silent", or "UI-only" event listeners?

Un-curry top-level functions

Idea:

• Record "natural" arity of top-level functions.
• When a LApp’s arity is equal to the natural arity, generate a direct call.
• Otherwise, generate a function “waiting for” the rest parameters (and being curried).

Move from Effects to Control.ST

You should move from the Effects library to Control.ST as it is preferred.

Better representation of `LCon`

Currently idrisjs uses an array to represent data values and use array indexing as projection. However given that LCon really has a name field, and there is a LConstructor declaration, could we generate real JS “classes” matching the name and arity of LCon? The final classes may be:

function Nil_0() { }
function Cons_2($0, $1) { this.$0 = $0; this.$1 = $1 }
... new Cons_2(..., ...) // LCon
... a.$1 // LProj

Todo example not working

I have Idris 1.3.2. ex0 and ex1 work for me, but I was unable to get the todo example to work. It compiles and loads, but after I type in a todo task and hit enter, the task shows up with an x button, but the button doesn't delete it and I can't enter any more todo items (hitting enter in the text box does nothing). There are no errors in the console. I was trying to debug it by throwing some consoleLog statements in the pageLoop, but that gave me a weird compilation error, specifically:

                             Specifically:
                                     Type mismatch between
                                             DomRef a f g x
                                     and
                                             DomRef Nat TodoState TodoAction n

Also, I couldn't get the game example to compile:

idris: Erasure/getArity: definition not found for Data.Tree.Empty
CallStack (from HasCallStack):
  error, called at src/Idris/Erasure.hs:605:20 in idris-1.3.2-H43oTI1BNEN3lkGNxFuB7Z:Idris.Erasure

Your lib looks pretty cool and I'd like to actually use it for a little project if I can at least get the elm-like todo list example working.