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
Interesting .. How does this interplay with parametricity ? Doesn't this weaken the notion of parametricity ?
1 reply 0 retweets 3 likes -
Replying to @debasishg
No. Parametricity and types are only coincidentally related. No reason a parameter has to be of type Type, nor that anything else can't be a parameter. See the code snippet for a tiny example :).
1 reply 0 retweets 4 likes -
Replying to @edwinbrady @debasishg
Could you spell out what you mean by 'parameter'? Implicit argument? Or argument with zero multiplicity maybe?
1 reply 0 retweets 0 likes
Replying to @atacratic @debasishg
Something where the value doesn't affect the function's behaviour. So, yes, zero multiplicity, in practice.
1:32 PM - 28 Jan 2019
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.