Documentation

SystemF is powerful enough to define Church Booleans.

>>> runLoud $ spec_ SysFStar >> churchBooleansScript
-- 1. Definitions
-----------------
--
λ» :define Bool : ⋆ = ∀ r → r → r → r
λ» :define True : Bool = λ r t f → t
λ» :define False : Bool = λ r t f → f
--
-- 2. Functions
---------------
--
-- Bool values are itself an if statement
λ» :define not : Bool → Bool = λ x → x Bool False True
λ» :define and : Bool → Bool → Bool = λ x y → x Bool y False
--
-- 3. Examples
--------------
--
-- One have to look carefully to distinguish the results :)
λ» :example and True True
↪ λ r t f → t : ∀ r → r → r → r
--
λ» :example and True False
↪ λ r t f → f : ∀ r → r → r → r
--
λ» :example and False True
↪ λ r t f → f : ∀ r → r → r → r
--
-- 4. Extras
------------
--
-- Note the usage of impredicativity.
λ» :example not
↪ λ x → x (∀ r → r → r → r) (λ r t f → f) (λ r t f → t)
: (∀ r → r → r → r) → ∀ r → r → r → r
--
λ» :example and
↪ λ x y → x (∀ r → r → r → r) y (λ r t f → f)
: (∀ r → r → r → r) → (∀ r → r → r → r) → ∀ r → r → r → r
∎

Examples of built-in Booleans. We need dependent types to be able to use dependent 𝔹-elim.

>>> runLoud $ spec_ (MartinLof 0) >> booleansScript
-- 1. Constants
---------------
--
λ» :example 𝔹
↪ 𝔹 : 𝓤
--
λ» :example true
↪ true : 𝔹
--
λ» :example false
↪ false : 𝔹
--
-- 2. Non-dependent elimination: if
-----------------------------------
--
λ» :define if : ∀ r → 𝔹 → r → r → r
              = λ r b t f → 𝔹-elim (λ _ → r) t f b
--
-- 3. Some simple functions on Booleans
---------------------------------------
--
-- 3.1. Negation, not
--
λ» :define not : 𝔹 → 𝔹 = λ b → if 𝔹 b false true
--
λ» :example not
↪ λ b → 𝔹-elim (λ _ → 𝔹) false true b : 𝔹 → 𝔹
--
λ» :example not true
↪ false : 𝔹
--
λ» :example not false
↪ true : 𝔹
--
-- 3.2. Conjunction, and
--
λ» :define and : 𝔹 → 𝔹 → 𝔹 = λ x y → if 𝔹 x y false
--
λ» :example and
↪ λ x y → 𝔹-elim (λ _ → 𝔹) y false x : 𝔹 → 𝔹 → 𝔹
--
λ» :example and true true
↪ true : 𝔹
--
λ» :example and true false
↪ false : 𝔹
--
λ» :example and false true
↪ false : 𝔹
--
λ» :example and false false
↪ false : 𝔹
--
-- 4. Using dependent elimination
---------------------------------
--
λ» :define contrived
: ∏ (b : 𝔹) → 𝔹-elim (λ _ → 𝓤) 𝔹 ℕ b
= λ b → 𝔹-elim (λ p → 𝔹-elim (λ _ → 𝓤) 𝔹 ℕ p) true 0 b
--
λ» :example contrived
↪ λ b → 𝔹-elim (λ p → 𝔹-elim (λ _ → 𝓤) 𝔹 ℕ p) true 0 b
: ∏ (b : 𝔹) → 𝔹-elim (λ _ → 𝓤) 𝔹 ℕ b
--
λ» :example contrived true
↪ true : 𝔹
--
λ» :example contrived false
↪ 0 : ℕ
∎

Primitive operations can be more powerful.

Note how we defined the Value:

data ValueIntro err s a
    ...
    | ValueTrue
    | ValueFalse
    ...

data ValueElim err s a
    ...
    | ValueAnd (ValueElim err s a) (ValueElim err s a)
    ...

By construction, there cannot be literal Boolean in evaluated ValueAnd. Following script demonstrates this functionality:

>>> runLoud $ spec_ SysFStar >> booleansPrimScript
-- 1. Using elimination
-----------------------
--
λ» :define if : ∀ r → 𝔹 → r → r → r
              = λ r b t f → 𝔹-elim (λ _ → r) t f b
λ» :define and : 𝔹 → 𝔹 → 𝔹 = λ x y → if 𝔹 x y false
--
λ» :example and
↪ λ x y → 𝔹-elim (λ _ → 𝔹) y false x : 𝔹 → 𝔹 → 𝔹
--
λ» :example and true true
↪ true : 𝔹
--
λ» :example and true false
↪ false : 𝔹
--
λ» :example and false true
↪ false : 𝔹
--
λ» :example and false false
↪ false : 𝔹
--
-- 1.1. Partial evaluation
--
-- Because we scrutinise the first argument, following expressions reduce (well):
λ» :example λ b → and true b : 𝔹 → 𝔹
↪ λ b → b : 𝔹 → 𝔹
--
λ» :example λ b → and false b : 𝔹 → 𝔹
↪ λ b → false : 𝔹 → 𝔹
--
-- ... but these doesn't:
λ» :example λ b → and b true : 𝔹 → 𝔹
↪ λ b → 𝔹-elim (λ _ → 𝔹) true false b : 𝔹 → 𝔹
--
λ» :example λ b → and b false : 𝔹 → 𝔹
↪ λ b → 𝔹-elim (λ _ → 𝔹) false false b : 𝔹 → 𝔹
--
-- 2. Built-in primitive
------------------------
--
λ» :define and# : 𝔹 → 𝔹 → 𝔹 = λ x y → 𝔹-and x y
--
λ» :example and#
↪ λ x y → 𝔹-and x y : 𝔹 → 𝔹 → 𝔹
--
λ» :example and# true true
↪ true : 𝔹
--
λ» :example and# true false
↪ false : 𝔹
--
λ» :example and# false true
↪ false : 𝔹
--
λ» :example and# false false
↪ false : 𝔹
--
-- 2.1. Partial evaluation
--
-- With primitive and we get more aggressive reduction behaviour
λ» :example λ b → and# true b : 𝔹 → 𝔹
↪ λ b → b : 𝔹 → 𝔹
--
λ» :example λ b → and# false b : 𝔹 → 𝔹
↪ λ b → false : 𝔹 → 𝔹
--
λ» :example λ b → and# b true : 𝔹 → 𝔹
↪ λ b → b : 𝔹 → 𝔹
--
λ» :example λ b → and# b false : 𝔹 → 𝔹
↪ λ b → false : 𝔹 → 𝔹
--
-- In fact, literal cannot be in evaluated and-expression:
λ» :example λ x y z → and# (and# x true)
                           (and# (and# y true) z)
                : 𝔹 → 𝔹 → 𝔹 → 𝔹
↪ λ x y z → 𝔹-and x (𝔹-and y z) : 𝔹 → 𝔹 → 𝔹 → 𝔹
--
λ» :example λ x y z → and# (and# x false)
                           (and# (and# y true) z)
                : 𝔹 → 𝔹 → 𝔹 → 𝔹
↪ λ x y z → false : 𝔹 → 𝔹 → 𝔹 → 𝔹
∎