Church.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
module Temp where

type Point f = forall a. a -> f a
data Nat = Z | S Nat

type family Apply n f x where
  Apply Z f x = x
  Apply (S n) f x = f (Apply n f x)

data Church (n :: Nat) where
  Church :: (forall f x. Point f -> x -> Apply n f x) -> Church n

zero :: Church Z
zero = Church $ \f x -> x

one :: Church (S Z)
one = Church $ \f x -> f x

two :: Church (S (S Z))
two = Church $ \f x -> f (f x)