Documentation

>>> runLoud $ spec_ CoCStar >> quarkSyntaxScript
-- Using quarks we can form a variant of Booleans
--
-- 1. Type
----------
--
λ» :define Boolean : ⋆ = {:false :true}
--
-- 2. Constructors
------------------
--
λ» :define True : Boolean = :true
λ» :define False : Boolean = :false
--
-- 3. Elimination
-----------------
--
λ» :define if
: ∀ r → Boolean → r → r → r
= λ r b t f → ℚ-elim (λ _ → r) b {:false → f;:true → t}
--
-- 4. Examples
--------------
--
λ» :define not : Boolean → Boolean
               = λ b → if Boolean b False True
--
λ» :example not
↪ λ b → ℚ-elim (λ _ → {:false :true}) b {:false → :true
                                        ;:true → :false}
: {:false :true} → {:false :true}
--
λ» :example not True
↪ :false : {:false :true}
--
λ» :example not False
↪ :true : {:false :true}
∎

This script demonstrates usage of quarks for making records, and defines a Monad using RankNTypes approach.

>>> runLoud $ spec_ CoCStar >> monadScript
-- 1. Class
-----------
--
λ» :define MonadMethods = {:fmap :join :pure}
λ» :define Monad'
: (⋆ → ⋆) → MonadMethods → ⋆
= λ M q → ℚ-elim (λ _ → ⋆)
                 q
                 {:fmap → (∀ A → ∀ B → (A → B) → M A → M B)
                 ;:join → (∀ A → M (M A) → M A)
                 ;:pure → (∀ A → A → M A)}
λ» :define Monad
: (⋆ → ⋆) → ⋆ = λ M → ∏ (q : MonadMethods) → Monad' M q
--
-- 2. Identity
--------------
--
λ» :define Identity : ⋆ → ⋆ = λ A → A
λ» :define MonadIdentity
: Monad Identity = λ q → ℚ-elim (λ q₁ → Monad' Identity q₁)
                                q
                                {:fmap → (λ _ _ f → f)
                                ;:join → (λ _ x → x)
                                ;:pure → (λ _ x → x)}
--
-- 3. Proxy
-----------
--
λ» :define Proxy : ⋆ → ⋆ = λ _ → ⊤
λ» :define MonadProxy
: Monad Proxy = λ q → ℚ-elim (λ q₁ → Monad' Proxy q₁)
                             q
                             {:fmap → (λ _ _ _ _ → I)
                             ;:join → (λ _ _ → I)
                             ;:pure → (λ _ _ → I)}
--
-- 4. Reader
------------
--
λ» :define Reader : ⋆ → ⋆ → ⋆ = λ E A → E → A
λ» :define MonadReader
: ∀ E → Monad (Reader E)
= λ E q → ℚ-elim (λ q₁ → Monad' (Reader E) q₁)
                 q
                 {:fmap → (λ A B ab ea e → ab (ea e))
                 ;:join → (λ A eea e → eea e e)
                 ;:pure → (λ A a e → a)}
--
-- 5. Polymorphic usage
-----------------------
--
λ» :define void
: ∏ (M : (⋆ → ⋆)) → Monad M → ∀ A → M A → M ⊤
= λ M $M A m → $M :fmap A ⊤ (λ _ → I) m
--
λ» :example void Identity
                 MonadIdentity
                 (∀ X → X → X)
                 (λ X x → x)
↪ I : ⊤
--
λ» :define env = {:bar :foo}
--
λ» :example void (Reader env) (MonadReader env) env (λ e →
                                                         e)
↪ λ e → I : {:bar :foo} → ⊤
∎