Church encoding demonstration

church.hs

#!/usr/bin/env stack
-- stack --resolver lts-14.7 script

-- How I run it:
-- fswatch -o src | xargs -n1 -I{} sh -c 'clear && ./src/church.hs'

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE NoImplicitPrelude #-}

module ChurchEnc where

import Protolude (IO, Text, putText, show)
import qualified Data.Bool as Hask
import Data.Semigroup ((<>))
import qualified GHC.Natural as Hask
import qualified Prelude

--------------------------------------------------------------------
--------------------------- Booleans -------------------------------
--------------------------------------------------------------------

type Boolean = forall a . a -> a -> a

true :: Boolean
true x _ = x

false :: Boolean
false _ y = y

toBoolean :: Boolean -> Hask.Bool
toBoolean b = b Hask.True Hask.False

fromBoolean :: Hask.Bool -> Boolean
fromBoolean Hask.True  = true
fromBoolean Hask.False = false

not :: Boolean -> Boolean
not b t f = b f t

or :: Boolean -> Boolean -> Boolean
or a b t f = a t (b t f) -- a a b

and :: Boolean -> Boolean -> Boolean
and a b t f = a (b t f) f -- a b a

-- xor :: Boolean -> Boolean -> Boolean
-- xor = notImplemented

testBooleans :: IO ()
testBooleans = do
  putText "\n--- Boolean <-> Bool isomorphism ---"
  putText ("toBoolean true = " <> toStr true)
  putText ("toBoolean false = " <> toStr false)
  putText ("fromBoolean True  = " <> toStr (fromBoolean Hask.True))
  putText ("fromBoolean False = " <> toStr (fromBoolean Hask.False))

  putText "\n--- not ---"
  putText ("not true  = " <> toStr (not true))
  putText ("not false = " <> toStr (not false))

  putText "\n--- or ---"
  putText ("false `or` false = " <> toStr (false `or` false))
  putText ("false `or` true  = " <> toStr (false `or` true))
  putText ("true  `or` false = " <> toStr (true `or` false))
  putText ("true  `or` true  = " <> toStr (true `or` true))

  putText "\n--- and ---"
  putText ("false `and` false = " <> toStr (false `and` false))
  putText ("false `and` true  = " <> toStr (false `and` true))
  putText ("true  `and` false = " <> toStr (true `and` false))
  putText ("true  `and` true  = " <> toStr (true `and` true))

  putText "\n--- xor ---"
  -- putText ("false `xor` false = " <> toStr (false `xor` false ))
  -- putText ("false `xor` true  = " <> toStr (false `xor` true  ))
  -- putText ("true `xor` false  = " <> toStr (true  `xor` false ))
  -- putText ("true `xor` true   = " <> toStr (true  `xor` true  ))
 where
  toStr :: Boolean -> Text
  toStr churchBool =
    let haskellBool = toBoolean churchBool in show haskellBool

--------------------------------------------------------------------
----------------------- Natural numbers ----------------------------
--------------------------------------------------------------------

type Natural = forall a . (a -> a) -> a -> a

toHaskNatural :: Natural -> Hask.Natural
toHaskNatural n = n Prelude.succ 0

fromHaskNatural :: Hask.Natural -> Natural
fromHaskNatural 0 = \_ x -> x
fromHaskNatural n = \f x ->
  let m :: Natural
      m = fromHaskNatural (Prelude.pred n)
  in  f (m f x)

zero :: Natural
zero _ x = x -- zero f = id

one :: Natural
one f x = f x
-- one f = f
-- one f x = f (zero f x)
-- one = id

testNaturalNumbers :: IO ()
testNaturalNumbers = do
  putText ("toHaskNatural zero = " <> show (toHaskNatural zero))
  putText ("toHaskNatural one = " <> show (toHaskNatural one))


--------------------------------------------------------------------
---------------------------- Main ----------------------------------
--------------------------------------------------------------------

main :: IO ()
main = do
  putText "---- Encoding Demo ---- "
  testBooleans

  putText "\n--- Naturals ---"
  testNaturalNumbers