Just procrastinated so hard I set up a blog and wrote about linearity and erasure in Idris 2. https://www.type-driven.org.uk/edwinb/linearity-and-erasure-in-idris-2.html … I'm probably not going to make a habit of this...
-
-
Just add open functions and you get first class typeclasses
-
This is what
@Augustsson suggested too, but we already have them! I think there will be other interesting generic programming we can do though. - 2 more replies
New conversation -
-
-
Can you write flatten (or any of the other gradual typing examples from my SNAPL paper https://drops.dagstuhl.de/opus/volltexte/2019/10549/ …)?
-
I think it's possible. Although I'd hope not to end up in a situation where I had to! I might have a go anyway...
- 1 more reply
New conversation -
-
-
Typecase is a good way to do type classes.
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.