DepTypeFun.hs

{-# LANGUAGE GADTs, ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds, KindSignatures #-}
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

data Nat = Z | S Nat

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

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

data SNat n where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)


toNum :: Num m => SNat n -> m
toNum SZ = 0
toNum (SS n) = 1 + toNum n

-- Smart constructors

sZ :: SNat Z
sZ = SZ

sS :: SNat n -> SNat (S n)
sS n = SS n


add :: SNat m -> SNat n -> SNat (m :+ n)
add SZ     n = n
add (SS m) n = sS(add m n)

mult :: SNat m -> SNat n -> SNat (m :* n)
mult SZ _ = SZ
mult (SS m) n = (mult m n) `add` n

two = sS $ sS sZ
four :: SNat ('S ('S ('S ('S 'Z))))
four = two `mult` two


-- Singletons inlined

class SRep n where
  single :: SNat n

instance SRep Z where
  single = SZ

instance SRep n => SRep (S n) where
  single = SS (single :: SNat n)

two' :: SNat('S ('S 'Z))
two' = single


data SInst (n :: Nat) where
  SInst :: SRep n => SInst n

sInst :: SNat n -> SInst n
sInst SZ     = SInst
sInst (SS n) = case sInst n of
                 SInst -> SInst


-- Making life difficult

data (:==:) a b where
  Refl :: x :==: x

cong :: a :==: b -> f a :==: f b
cong Refl = Refl

trans :: a :==: b -> b :==: c -> a :==: c
trans Refl Refl = Refl


nPlusZero :: SNat n -> (n :+ Z) :==: n
nPlusZero SZ = Refl
nPlusZero (SS n) = cong (nPlusZero n)

sucDist :: SNat n -> SNat m -> n :+ (S m) :==: S (n :+ m)
sucDist SZ m     = Refl
sucDist (SS n) m = cong (sucDist n m)

plusComm :: SNat n -> SNat m -> (n :+ m) :==: (m :+ n)
plusComm n SZ     = nPlusZero n
plusComm n (SS m) = trans (sucDist n m) (cong (plusComm n m))


add2 :: SNat m -> SNat n -> SNat (n :+ m)
add2 m n = case plusComm m n of
             Refl -> add m n

three = sS two'

five = two' `add2` three


main :: IO ()
main = do
   putStr "toNum four == "
   print $ toNum four
   putStr "toNum five == "
   print $ toNum five