Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- #!/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
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement