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 …
I have no idea, I'm afraid. Although it's not a thing I ever intend for Idris. And there is a distinction between forall and pi now which may be relevant.
-
-
Univalence says that isomorphic types are equal. So `(Bool, Bool) = Bool -> Bool`. So `describe (Bool, Bool) = describe (Bool -> Bool)`. Doesn't mean you need parametricity, just that pattern matching on types is serverely restricted (iiuc).
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.