module Data.Numerals where
import Prelude hiding (succ, exp)
newtype N = N (forall a . (a -> a) -> a -> a)
un (N x) = x
zero :: N
zero = N ( \f a -> a )
succ :: N -> N
succ n = N ( \f a -> f (un n f a) )
one:: N
one = succ zero
add, mul :: N -> N -> N
add m n = N( \f a -> un m f (un n f a) )
mul m n = N( \f a -> un m (un n f) a )
exp :: N -> N -> N
exp m n = un n (mul m) one
exp2 :: N -> N -> N
exp2 m n = N (\f a -> un n (un m) f a)
test1 = un (exp two three) (+1) 0
where two = succ one
three = succ two
test2 = un (exp2 two three) (+1) 0
where two = succ one
three = succ two
f1:: (forall a. a->a) -> b -> b
f1 g x = g x
testf1 = f1 id True
foo:: forall c notimportant. (c->c) -> notimportant
foo = undefined
newtype W = W{unW :: forall a. a -> a}
f2:: W -> b -> b
f2 g x = unW g x
testf2 = f2 (W id) True
testf2' = foo (\x -> W(f2 x))