長さを表す型付きリストで型安全なlength, zip, head, tail, append

lengthList.hs

{-# LANGUAGE DataKinds, GADTs, KindSignatures, FlexibleInstances, FlexibleContexts, TypeFamilies #-}
import Control.Applicative

data Nat = Zero | Succ Nat
type family Plus (n :: Nat) (m :: Nat) :: Nat
type instance Plus (Succ n) m = Succ (Plus n m)
type instance Plus Zero m = m

data LengthList n a where
  Nil :: LengthList Zero a
  (:::) :: a -> LengthList n a -> LengthList (Succ n) a
infixr :::

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

lengthL :: LengthList n a -> Int
lengthL (_ ::: xs) = 1 + lengthL xs
lengthL Nil = 0

instance Functor (LengthList n) where
  fmap f (x ::: xs) = f x ::: fmap f xs
  fmap _ Nil = Nil

instance Applicative (LengthList Zero) where
  pure _ = Nil
  Nil <*> Nil = Nil

instance (Applicative (LengthList n)) => Applicative (LengthList (Succ n)) where
  pure a = a ::: pure a
  (f ::: fs) <*> (x ::: xs) = f x ::: (fs <*> xs)

instance (Show a) => Show (LengthList n a) where
  show x = show $ (lengthL x, toList x)

safeZip :: LengthList n a -> LengthList n b -> LengthList n (a,b)
safeZip Nil Nil = Nil
safeZip (x ::: xs) (y ::: ys) = (x,y) ::: (safeZip xs ys)

safeHead :: LengthList (Succ n) a -> a
safeHead (x ::: _) = x

safeTail :: LengthList (Succ n) a -> LengthList n a
safeTail (_ ::: xs) = xs

(+++) :: LengthList n a -> LengthList m a -> LengthList (Plus n m) a
(x ::: xs) +++ y = x ::: (xs +++ y)
Nil +++ y = y

main = do
  let list4 = 1 ::: 2 ::: 3 ::: 4 ::: Nil
  let listd = 'a' ::: 'b' ::: 'c' ::: 'd' ::: Nil
  let list2 = 1 ::: 2 ::: Nil
  print $ listd
  print $ list4
  
  print $ safeZip list4 listd
--  print $ safeZip listd list2  <-- compilation error !!

  print $ safeHead list4
--  print $ safeHead Nil  <-- compilation error !!
  print $ safeTail listd
  
  print $ list4 +++ list2 +++ list4
  
  let listA = 1.2 ::: 3.2 ::: 9.5 ::: Nil
  let listB = 199 ::: 300 ::: 49 ::: Nil
  print $ (+) <$> listA <*> listB