3 ms·
Can a dependently typed list be used in the common case where the length of the list is not known at compile time?
by lonelappde 7y ago
Can a dependently typed list be used in the common case where the length of the list is not known at compile time?
- andreabedini 7y agoYes, that’s the whole point of dependent types: types can depend on (runtime) values.
- Legogris 7y agoYes. Just like with generics, you can parametrize them, for example in Idris you have the type `Vect n a`, being a list of type `a` with length `n`. An append function could look like this: app : Vect n a -> Vect m a -> Vect (n + m) a app Nil ys = ys app (x :: xs) ys = x :: app xs ys Source: https://www.idris-lang.org/example/ https://www.idris-lang.org/example/
- whateveracct 7y agoYep - we can even do this today in Haskell without -XDependentTypes :) using things like singletons