Arc Forum | data Nat = Zero | Succ Nat I don't think this itself would be called Church n...

Arc Forum

2 points by rocketnia 3870 days ago | link | parent

  data Nat = Zero | Succ Nat

I don't think this itself would be called Church numerals, but it's related. The Church encoding takes an ADT definition like this one and looks at it as a polymorphic type. Originally we have two constructors for Nat whose types are as follows:

  Zero : Nat
  Succ : (Nat -> Nat)

These two constructors are all you need to build whatever natural number you want:

  buildMyNat : Nat -> (Nat -> Nat) -> Nat
  buildMyNat zero succ = succ (succ (succ zero)))

We could make this function more general by abstracting it over any type, not just Nat:

  buildMyNat : a -> (a -> a) -> a

This type (a -> (a -> a) -> a) is the type of a Church numeral.

While it's more general in this way, I think sometimes it's a bit less powerful. Dependently typed languages often provide induction and recursion support for ADT definitions, but I think they can't generally do that for Church-encoded types. (I could be wrong.)

For something more interesting, we can go through the same process to build a Church encoding for my binary integer example:

  data OneOrMore = One | Double OneOrMore | DoublePlusOne OneOrMore
  data Int = Negative OneOrMore | Zero | Positive OneOrMore
  
  buildMyInt :
    OneOrMore ->                  -- One
    (OneOrMore -> OneOrMore) ->   -- Double
    (OneOrMore -> OneOrMore) ->   -- DoublePlusOne
    (OneOrMore -> Int) ->         -- Negative
    Int ->                        -- Zero
    (OneOrMore -> Int) ->         -- Positive
      Int
  
  buildMyInt :
    a ->          -- One
    (a -> a) ->   -- Double
    (a -> a) ->   -- DoublePlusOne
    (a -> b) ->   -- Negative
    b ->          -- Zero
    (a -> b) ->   -- Positive
      b