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 …
-
-
This Tweet is unavailable.
-
We have one of these in the Prelude: the : (0 a : Type) -> a -> a the _ x = x
- 3 more replies
-
-
-
Datatype-generic programming?
-
There is probably some fun to be had there, yes
End of conversation
New conversation -
-
-
This Tweet is unavailable.
-
Intriguing...
End of conversation
-
-
-
I have a use case for this!
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
-
-
not sure it's exactly the same, but did you see work by
@odersky on match type for dotty? Doc here: https://dotty.epfl.ch/docs/reference/new-types/match-types.html … Pr:https://github.com/lampepfl/dotty/pull/4964 … -
Or typescript conditionals (I feel sorry to be the one to bring ts into such a conversation)
- 1 more reply
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.