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
Is there any way to extract sum/product structure from this?
1 reply 0 retweets 2 likes -
Replying to @milessabin
No, you can only look at the type constructor names, but don't get access to their data constructors. Elaborator reflection could do this, potentially. And maybe we could make it accessible at run time... but not just now.
1 reply 0 retweets 1 like -
Replying to @edwinbrady
Is there a deep reason for that (as opposed to lack of resources)?
1 reply 0 retweets 0 likes
Replying to @milessabin
I can't think of what the type of such an operation would be
12:05 PM - 28 Jan 2019
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.