Sometimes when I say types are first class in Idris, someone (quite reasonably) points out you can't pattern match on them. Well, here we go...https://gist.github.com/edwinb/25cd0449aab932bdf49456d426960fed …
-
Show this thread
-
Replying to @edwinbrady
That is pretty cool but the free theorems you get from the type signatures become a lot weaker, right? How does that interact with the automatic implementation of signatures the compiler can generate?
1 reply 0 retweets 0 likes
Replying to @mgttlinger
If your type says you're allowed to inspect an argument then there are more implementations available. So, if you don't want that, don't do that!
3:00 AM - 26 Jan 2019
from Edinburgh, Scotland
0 replies
0 retweets
1 like
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.