Created
September 23, 2019 16:40
-
-
Save kfl/8d3c061b77a44b7bee0201e9d1aec735 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment