dependent types

dependent.hs

data Vect :: Nat -> * -> * where
  Cons :: KnownNat n => a -> Vect (n - 1) a -> Vect n a
  Nil :: (KnownNat n, 0 <= n) => Vect n a

k :: Vect 1 Int
k = Cons 1 Nil

u :: Vect 0 Int
u = Nil

j = vhead k

p = vtail k

vhead :: KnownNat n => Vect (n + 1) a -> a
vhead (Cons x _) = x

vtail :: (KnownNat n, n ~ (n + 1 - 1)) => Vect (n + 1) a -> Vect n a
vtail Nil         = Nil
vtail (Cons _ xs) = xs

vzip :: Vect n a -> Vect n b -> Vect n (a, b)
vzip Nil Nil                 = Nil
vzip (Cons x xs) (Cons y ys) = Cons (x, y) $ vzip xs ys

vindex :: (KnownNat n, KnownNat i, i <= n - 1) => Proxy i -> Vect n a -> a
vindex (pi :: Proxy i) (Cons x xs) =
  case natVal pi of
    0 -> x
    _ -> vindex (Proxy :: Proxy (i - 1)) xs