ad-hoc overloading with interfaces

veccy.idr

import Data.Vect

%hide List.Nil

interface Addable (a : Type) (b : Type) (c : Type) | a, b where
  add : a -> b -> c

-- it's redundant to case-split this for vectors, but just for example
Addable (Vect n a) (Vect Z a) (Vect n a) where
  add xs _ = xs

Addable (Vect n a) (Vect (S m) a) (Vect (n + S m) a) where
  add xs ys = xs ++ ys

Addable a (Vect n a) (Vect (S n) a) where
  add x xs = x::xs

ex1 : Vect 5 Int
ex1 = [1, 2, 3, 4, 5]

ex2 : Vect 5 Int
ex2 = add ex1 []

ex3 : Vect 10 Int
ex3 = add ex1 ex1

ex4 : Vect 6 Int
ex4 = add (the Int 0) ex1