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
Replying to
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.
Note that you can see this in action in Idris 2, a.k.a Blodwen. :)
1