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/