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...
-
-
-
Replying to @fancytypes
You can tell I have exams to mark! (typecase is fun, although I still haven't found a use for it... I bet I will...)
3 replies 0 retweets 2 likes -
Replying to @edwinbrady @fancytypes
Just add open functions and you get first class typeclasses
1 reply 0 retweets 0 likes -
Replying to @BetaZiliani @fancytypes
This is what
@Augustsson suggested too, but we already have them! I think there will be other interesting generic programming we can do though.1 reply 0 retweets 0 likes -
You have Open functions?
1 reply 0 retweets 0 likes
No, I mean first class type classes (or rather, interfaces)
4:04 AM - 11 Jan 2020
0 replies
0 retweets
0 likes
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.