I'm probably being a pedant and/or asking for trouble, but couldn't you theoretically make a code type for the Idris Universe(s) and then use that to pattern match on Idris types? Sure, it breaks theorems for free (which is just the fact that parametric polymorphism must be natural), but you need something like that for a self-hosting compiler. If HoTT got folded in, then you could even attempt naturality proofs for non-parametric polymorphic functions in the places where it needs to be ensured.
One of the most interesting languages at the moment.
I think it is still today. It allows even more concise code than most other languages.
Great audio. Thanks
Brilliant talk. Thanks!
I'm probably being a pedant and/or asking for trouble, but couldn't you theoretically make a code type for the Idris Universe(s) and then use that to pattern match on Idris types? Sure, it breaks theorems for free (which is just the fact that parametric polymorphism must be natural), but you need something like that for a self-hosting compiler. If HoTT got folded in, then you could even attempt naturality proofs for non-parametric polymorphic functions in the places where it needs to be ensured.
btw Idris 2 has type-case, in case you want to give it a try:
gist.github.com/edwinb/25cd0449aab932bdf49456d426960fed
github.com/edwinb/Idris2