GADTsを使った長さを型に持たせたリスト演算とGADTsをleibniz equalityでエンコードする話

GadtVector.hs

{-# LANGUAGE Rank2Types, TypeOperators, TypeFamilies, KindSignatures, GADTs #-}
module GadtVector where
import Prelude hiding (head, tail, map, zipWith, reverse, foldr)

data Z   -- zero
data S a -- succ

data Vec :: * -> * -> * where
  Nil  :: Vec a Z
  Cons :: a -> Vec a n -> Vec a (S n)

infixr 5 `Cons`

head :: Vec a (S n) -> a
head (Cons x _) = x

tail :: Vec a (S n) -> Vec a n
tail (Cons _ xs) = xs

map :: (a -> b) -> Vec a n -> Vec b n
map _ Nil         = Nil
map f (Cons x xs) = f x `Cons` map f xs

zipWith :: (a -> b -> c) -> Vec a n -> Vec b n -> Vec c n
zipWith _ Nil         Nil         = Nil
zipWith f (Cons x xs) (Cons y ys) = f x y `Cons` zipWith f xs ys

snoc :: Vec a n -> a -> Vec a (S n)
snoc Nil         y = Cons y Nil
snoc (Cons x xs) y = Cons x (snoc xs y)

reverse :: Vec a n -> Vec a n
reverse Nil         = Nil
reverse (Cons x xs) = reverse xs `snoc` x

type family (:+:) m n
type instance Z   :+: n   = n
type instance S m :+: n   = S (m :+: n)

append :: Vec a m -> Vec a n -> Vec a (m :+: n)
append Nil         ys = ys
append (Cons x xs) ys = Cons x (append xs ys)

toList :: Vec a n -> [a]
toList Nil         = []
toList (Cons x xs) = x:toList xs

data Nat :: * -> * where
  Z :: Nat Z
  S :: Nat n -> Nat (S n)

{-
fromList :: Nat n -> [a] -> Vec a n
fromList Z     []     = Nil
fromList (S n) (x:xs) = Cons x (fromList n xs)
fromList _     _      = error "wrong length"
-}

data VecAny :: * -> * where
  VecAny :: Vec a n -> VecAny a

fromList :: [a] -> VecAny a
fromList [] = VecAny Nil
fromList (x:xs) = case fromList xs of
  VecAny ys -> VecAny (Cons x ys)

useVecAny = case fromList [1..5] of
  VecAny vec -> toList $ vec `append` vec

data (:=:) :: * -> * -> * where
  Refl :: a :=: a

equalLength :: Vec a m -> Vec b n -> Maybe (m :=: n)
equalLength Nil Nil = Just Refl
equalLength (Cons x xs) (Cons y ys) =
  case equalLength xs ys of
    Just Refl -> Just Refl
    Nothing   -> Nothing
equalLength _ _ = Nothing

useEqualLen :: Vec a m -> Vec b (S n) -> (a, b)
useEqualLen v w = case equalLength v w of
  Just Refl -> head (zipWith (,) v w)
  Nothing   -> error "different length"

-- EqualityでGADTsをエンコードする。equality自体はGADTsを使っている。
type family Pred n
type instance Pred (S n) = n

data Vec' a n
  = Nil' (n :=: Z)
  | Cons' a (Vec' a (Pred n))

nil' :: Vec' a Z
nil' = Nil' Refl

head' :: Vec' a (S n) -> a
head' (Cons' a _) = a

tail' :: Vec' a (S n) -> Vec' a n
tail' (Cons' _ xs) = xs

map' :: (a -> b) -> Vec' a n -> Vec' b n
map' _ (Nil' p)     = Nil' p
map' f (Cons' x xs) = f x `Cons'` map' f xs

zipWith' :: (a -> b -> c) -> Vec' a n -> Vec' b n -> Vec' c n
zipWith' _ (Nil' p)     (Nil' _)     = Nil' p
zipWith' f (Cons' x xs) (Cons' y ys) = f x y `Cons'` zipWith' f xs ys

snoc' :: Vec' a (Pred n) -> a -> Vec' a n
snoc' (Nil' p)     y = Cons' y (Nil' p)
snoc' (Cons' x xs) y = Cons' x (snoc' xs y)

reverse' :: Vec' a n -> Vec' a n
reverse' (Nil' p)     = Nil' p
reverse' (Cons' x xs) = reverse' xs `snoc'` x

-- FOPより。こちらのequalityはRank2Typesで実現している。
newtype a :==: b = Proof { apply :: forall f. f a -> f b }

refl :: a :==: a
refl = Proof id

data Vec'2 a n
  = Nil'2 (n :==: Z)
  | Cons'2 a (Vec'2 a (Pred n))

nil'2 :: Vec'2 a Z
nil'2 = Nil'2 refl

head'2 :: Vec'2 a (S n) -> a
head'2 (Cons'2 a _) = a

tail'2 :: Vec'2 a (S n) -> Vec'2 a n
tail'2 (Cons'2 _ xs) = xs

map'2 :: (a -> b) -> Vec'2 a n -> Vec'2 b n
map'2 _ (Nil'2 p)     = Nil'2 p
map'2 f (Cons'2 x xs) = f x `Cons'2` map'2 f xs

zipWith'2 :: (a -> b -> c) -> Vec'2 a n -> Vec'2 b n -> Vec'2 c n
zipWith'2 _ (Nil'2 p)     (Nil'2 _)     = Nil'2 p
zipWith'2 f (Cons'2 x xs) (Cons'2 y ys) = f x y `Cons'2` zipWith'2 f xs ys

snoc'2 :: Vec'2 a (Pred n) -> a -> Vec'2 a n
snoc'2 (Nil'2 p)     y = Cons'2 y (Nil'2 p)
snoc'2 (Cons'2 x xs) y = Cons'2 x (snoc'2 xs y)

reverse'2 :: Vec'2 a n -> Vec'2 a n
reverse'2 (Nil'2 p)     = Nil'2 p
reverse'2 (Cons'2 x xs) = reverse'2 xs `snoc'2` x