she-0.0: examples/Vec.lhs

> {-# OPTIONS_GHC -F -pgmF she #-}
> {-# LANGUAGE GADTs, KindSignatures, TypeOperators #-}

> module Vec where

> import Control.Applicative

> data Nat = Z | S Nat

> data Vec :: {Nat} -> * -> * where
>   VNil :: Vec {Z} x
>   (:>) :: x -> Vec {n} x -> Vec {S n} x

> vtail :: Vec {S n} x -> Vec {n} x
> vtail (x :> xs) = xs

> vapp :: Vec {n} (s -> t) -> Vec {n} s -> Vec {n} t
> vapp VNil VNil = VNil
> vapp (f :> fs) (s :> ss) = f s :> vapp fs ss