Type level natural numbers

Main.purs

module Main where

import Control.Monad.Eff (Eff)
import Control.Monad.Eff.Console (CONSOLE, logShow)
import Data.Function (const)
import Prelude (Unit, (+))
import Type.Proxy (Proxy(..))

data Zero
data Succ a

type One   = Succ Zero
type Two   = Succ One
type Three = Succ Two

numPred :: forall a. Proxy (Succ a) -> Proxy a
numPred = const Proxy

class Number a where
    numValue :: Proxy a -> Int

instance numberZero :: Number Zero where
    numValue = const 0

instance numberSucc :: Number x => Number (Succ x) where
    numValue x = numValue (numPred x) + 1

three :: Proxy Three
three = Proxy

main :: forall e. Eff (console :: CONSOLE | e) Unit
main = logShow (numValue three)