people familiar with dependent types, what do you think of being able to choose between relevant
pi a -> ..
and irrelevant quantification
forall a -> ..
orthogonally from visibility
cs.brynmawr.edu/~rae/papers/20
Conversation
I definitely think it’s important. Wish it was in more dependently typed langs. Personally would prefer using multiplicities for this though. See quantitative type theory and linear Haskell.
1
1
Note that you can see this in action in Idris 2, a.k.a Blodwen. :)