{-# LANGUAGE GADTs, KindSignatures, DataKinds, StandaloneDeriving #-}
data Nat = Z | S Nat deriving (Show, Eq)
toInt Z = 0
toInt (S a) = 1 + toInt a
data Vector (a :: *) (n :: Nat) where -- Vector a (n :: Nat)
Nil :: Vector a Z
(:-) :: a -> Vector a n -> Vector a (S n)
infixr 5 :-
deriving instance Show a => Show (Vector a n)
vlength :: Vector a n -> Int
vlength = toInt . slength
slength :: Vector a n -> Nat
slength Nil = Z
slength (a :- b) = S (slength b)
type Two = S (S Z)
main = do
let vec = "Hello" :- "World" :- Nil :: Vector String Two
print vec
print $ slength vec
print $ vlength vec
