Peano.purs

-- | Type level Peano numbers in PureScript.
module Main where

import Prelude hiding (zero,one,add)

import Effect (Effect)
import Effect.Console (log)


foreign import kind Peano

foreign import data Succ :: Peano -> Peano
foreign import data Zero :: Peano

data PeanoProxy (a :: Peano) = PeanoProxyValue

class ShowPeano (a :: Peano) where
  reflectPeano :: PeanoProxy a -> Int

instance showPeanoZero :: ShowPeano Zero where
  reflectPeano _ = 0

instance showPeanoSucc :: ShowPeano p => ShowPeano (Succ p) where
  reflectPeano _ = 1 + reflectPeano (PeanoProxyValue :: PeanoProxy p)


class SuccPeano (input :: Peano) (output :: Peano) 
    | input -> output
    
instance succPeanoZero :: SuccPeano Zero (Succ Zero)
else 
instance succPeanoSucc :: SuccPeano s (Succ s)


class AddPeano (inputA :: Peano) (inputB :: Peano) (output :: Peano)
    | inputA inputB -> output

instance addPeanoZeroA :: AddPeano Zero b b
else
instance addPeanoZeroB :: AddPeano a Zero a
else
instance addPeanoSucc :: AddPeano a (Succ b) c => AddPeano (Succ a) b c


  
class ShowPeano b <= PeanoKindConstraint b
instance peanoTypeConstraint :: ShowPeano b => PeanoKindConstraint b


zero :: PeanoProxy Zero
zero = PeanoProxyValue

one :: PeanoProxy (Succ Zero)
one = PeanoProxyValue

five :: PeanoProxy (Succ (Succ (Succ (Succ (Succ Zero)))))
five = PeanoProxyValue


succ :: forall a b . SuccPeano a b => PeanoProxy a -> PeanoProxy b
succ _ = PeanoProxyValue

add :: forall a b c . AddPeano a b c => PeanoProxy a -> PeanoProxy b -> PeanoProxy c
add _ _ = PeanoProxyValue


main :: Effect Unit
main = do
  log $ show $ reflectPeano zero
  log $ show $ reflectPeano one
  log $ show $ reflectPeano $ succ one
  log $ show $ reflectPeano $ add one (succ one)
  log $ show $ reflectPeano $ add five (succ five)