3 ms·
Yes. 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 f
by Legogris 7y ago
Yes. 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/