Why is parametric polymorphism limited to just types? What if I want to write a function `(n : Nat) -> Fin n -> Fin n` that cannot pattern match on the value of `n`?
Conversation
I also would occasionally like to pattern match on types. Can't my type signature distinguish which parameters can be used in elim rules and which ones can't?
2
1
1
We will hopefully get type case in Idris 2 thanks to linearity.
1
1
3
as in type case would be allowed by default, but type variables (by default) would be inferred like {0 a : Type} ? that'd be great!
1
2
I don't think I understand this. Where can I learn more?
2
If we allow type case, then we would lose very nice reasoning properties we get through parametricity, e.g. that there is only one implementation of the identity function. However with linearity, we will know from the resource annotation whether we are casing on a type.
1
4
This is why I really love multiplicities on binders! 😍