Incidentally, the implementation of Idris 2, which I intend to write up Real Soon Now, will make experimentation with different front ends and back ends much easier. So if you want to try Lazy Idris, you "just" need to implement it on top of the type checker...
-
-
Show this threadThanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
I feel this is chasing a red herring. Lazy languages have strictness annotations. Strict ones have lazy annotations. And total ones set the don't care bit...
-
I agree. I like both defaults. It's either amusing or infuriating (depending on my mood) how often people tell me I picked the wrong (or right) default though...
- 4 more replies
New conversation -
-
-
Honestly, strictness in Idris is very much appreciated!
-
It certainly is by me :).
End of conversation
New conversation -
-
-
scheme? *ducks and runs*
-
I have considered this...
End of conversation
New conversation -
-
-
This Tweet is unavailable.
-
I don't have a keyboard big enough. Scheme, maybe :)
- 1 more reply
-
-
-
-
Namespaces in Idris 1 certainly help: I'm hoping Idris 2 will retain this excellent feature. I wish Haskell would adopt it.
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.