Development

.agda-lib

@@ -4,3 +4,4 @@ include:
   ./src/
   ./lib/stdlib/src/
   ./lib/stdlib++/src/
+  ./lib/categories

.gitignore

@@ -1,3 +1,4 @@
 docs/
+hs/
 *.agdai
 .#*

.gitmodules

@@ -4,3 +4,6 @@
 [submodule "lib/stdlib"]
 	path = lib/stdlib
 	url = https://github.com/agda/agda-stdlib
+[submodule "lib/categories"]
+	path = lib/categories
+	url = https://github.com/copumpkin/categories.git

Readme.agda

@@ -10,8 +10,13 @@
   A rendered and linked version of this readme can be found here:
   - https://metaborg.github.io/mj.agda/
 
-  This development has been tested against Agda 2.5.3 (and should also compile
-  with 2.6.0). If you have this installed, you should simply be able to run
+  The current development uses do-notation syntactic sugar
+  that is now part of Agda 2.5.4+ and will not compile with earlier versions.
+  The POPL paper does *not* use do-notation; you may want to download the
+  mj-1.0.0-popl18 release if you want a version compatible with the
+  paper and Agda 2.5.3.
+
+  If you have the right version of Agda installed, you should be able to run
   `make` in the project root. This will checkout the two dependencies in
   `./lib/` first and then build this `./Readme.agda` which serves as the main
   entrypoint to the development.
@@ -22,7 +27,7 @@
   for it. The html docs are syntax-highlighted and you can click
   references to navigate to their definitions.
 
-  There are some minor differences between the Agda code used in the
+  There are some differences between the Agda code used in the
   paper and this mechanization.  One general (but minor) discrepancy
   is that the definitions in the paper are typed in a manner that is
   not universe polymorphic.  However, the development makes extensive
@@ -223,9 +228,9 @@ open import Experiments.Infer
   point-free style.
 -}
 
-open import Experiments.Category
-open import Experiments.StrongMonad
-open import Experiments.STLCRefPointfree
+-- open import Experiments.Category
+-- open import Experiments.StrongMonad
+-- open import Experiments.STLCRefPointfree
 
 {-
   We briefly outline how these experiments relate to our paper.

default.nix

@@ -0,0 +1,23 @@
+{
+  pkgs ? (import <nixpkgs> {})
+}:
+
+let
+  # get nixplus
+  nixplus = import (pkgs.fetchgit {
+    url    = https://gitlab.ewi.tudelft.nl/aj.rouvoet/nixplus.nix.git;
+    sha256 = "0zla8sf6k1n0ggb2h416n0x4ganjr3lnrz4mv5blsfyakjhrrxha";
+    rev    = "e9d6d27e37e88d318dd5963b1751482c292ce36f";
+  });
+
+in nixplus.stdenv.mkDerivation rec {
+  version = "1.1.0";
+  name    = "mj.agda-${version}";
+  src     = ./.;
+
+  buildInputs = with nixplus; [
+    git
+    agdaPackages.Agda.v2_5_4
+  ];
+}
+

makefile

@@ -1,11 +1,17 @@
 VERSION = 1.0.0-SNAPSHOT
+AGDA_OPTS = --verbose=2
+AGDA = agda $(AGDA_OPTS)
 
 # some library paths
 docs/%.html: %.agda
-	agda $< --html --html-dir=./docs/
+	$(AGDA) $< --html --html-dir=./docs/
 
 %.agdai: %.agda
-	agda $<
+	$(AGDA) $<
+
+.PHONY: hs/%
+hs/%: src/%.agda
+	$(AGDA) --compile --compile-dir hs $<
 
 all: lib Readme.agdai
 
@@ -19,7 +25,11 @@ docs: lib docs/Readme.html
 	cp docs/Readme.html docs/index.html
 
 ### libraries
-lib: lib/stdlib/.git lib/stdlib++/.git
+lib: lib/stdlib/.git lib/stdlib++/.git lib/categories/.git
+
+lib/categories/.git:
+	git submodule update --init lib/categories
+	cd lib/categories
 
 lib/stdlib++/.git:
 	git submodule update --init lib/stdlib++

src/Categorical/Examples/Arith.agda

@@ -0,0 +1,88 @@
+module Categorical.Examples.Arith where
+{-
+  This example demonstrates how the *later* guard and fueled functions
+  can be used to build a definitional interpreter for a simple
+  arithmetic language.
+
+  This example does not involve intrinsically typed syntax or state.
+  It also doesn't necessitate fuel, because we could build the fixpoint in Agda;
+  but we do not allow that escape here.
+-}
+
+open import Level using () renaming (zero to lz)
+open import Data.Nat as Nat using (ℕ)
+open import Relation.Binary.PropositionalEquality using () renaming (refl to ≣-refl)
+
+open import Categories.Category
+open import Categories.Support.Equivalence
+
+open import Categorical.Ofe
+open import Categorical.Ofe.Cofe renaming (_⇨_ to _⇨-cofe_)
+open import Categorical.Ofe.Products
+open import Categorical.Ofe.Exponentials
+open import Categorical.Ofe.Later
+open import Categorical.Ofe.StepIndexed
+open import Categorical.Ofe.Properties
+
+-- we specialize here to ofes at universe level zero;
+-- all our types and such fit in there
+Cat = Ofes {lz}{lz}{lz}
+
+open import Categories.Object.Exponential Cat
+open import Categories.Object.Exponentiating Cat binary-products
+open import Categories.Object.BinaryProducts Cat
+open import Categories.Support.SetoidFunctions as SF using () renaming (→-to-⟶ to lift)
+
+open Category Cat
+open BinaryProducts binary-products
+
+private
+  data Exp-set : Set where
+    num : ℕ → Exp-set
+    add : Exp-set → Exp-set → Exp-set
+
+-- our values are just the natural numbers
+Val = set→setoid ℕ
+
+-- lift expressions to Ofe trivially
+Exp = Δ⁺ Exp-set
+
+module Elim (A : Ofe lz lz lz) where
+
+  Rec = (Exp ⇨ A)
+
+  -- eliminator of the Exp type
+  elim : (Rec ×-ofe (Δ⁺ ℕ)) ⇒ A →
+         (Rec ×-ofe (Exp ×-ofe Exp)) ⇒ A →
+         (Rec ×-ofe Exp) ⇒ A
+  _⟨$⟩_ (elim f g) (rec , num n) = f ⟨$⟩ (rec , n)
+  _⟨$⟩_ (elim f g) (rec , add e₁ e₂) = g ⟨$⟩ (rec , e₁ , e₂)
+  cong (elim f g) {x = rec , num _} (eq , ≣-refl) = cong f (eq , ≣-refl)
+  cong (elim f g) {x = rec , add _ _} (eq , ≣-refl) = cong g (eq , ≣-refl , ≣-refl)
+
+-- Make the syntax of manipulating exponentiating available
+module _ {X : Obj} where
+  open Exponentiating record { exponential = λ {A} → exp A X } public
+
+Eval = Exp ⇨ ⇀ Val
+
+eval-arith : ⊤ ⇒ Eval
+eval-arith = μ (Exp ⇨-cofe (⇀-cofe Val)) eval' (⇨-const (⇀-inhabited Val))
+  where
+    case-num : (Eval × Δ⁺ ℕ) ⇒ ⇀ Val
+    case-num = fuel SF.id ∘ π₂ {A = Eval}
+
+    case-add : (Eval × (Exp × Exp)) ⇒ ⇀ Val
+    case-add =
+        {!!}                                     -- add values
+      ∘ _⁂_ {C = Eval × Exp} eval eval          -- recursively evaluate the sub-expressions
+      ∘ ×-distrib-× {A = Eval}{B = Exp}{C = Exp} -- fiddling with arguments
+
+    eval' : Ofes [ ► Eval , Eval ]
+    eval' =
+      λ-abs _ (                                  -- building a function
+        Elim.elim (⇀ Val)                        -- eliminate the two expression-cases
+            case-num
+            case-add
+        ∘ first {C = Exp} rec-unfold             -- build the recursor
+      )

src/Categorical/Examples/BoolNum.agda

@@ -0,0 +1,114 @@
+{-# OPTIONS --show-implicit #-}
+module Categorical.Examples.BoolNum where
+{-
+  This example builds on Categorical.Examples.Arith
+
+  We add a type bool and the corresponding value and expressions.
+  To ensure soundness-by-construction we type the expression and value syntax.
+
+  The interpreter structure remains the same, but the expression-elimination
+  is more involved.
+-}
+
+open import Level using () renaming (zero to lz)
+open import Data.Nat as Nat using (ℕ)
+open import Relation.Binary.PropositionalEquality using () renaming (refl to ≣-refl)
+
+open import Categories.Category
+open import Categories.Support.Equivalence
+
+open import Categorical.Ofe
+open import Categorical.Ofe.Cofe renaming (_⇨_ to _⇨-cofe_)
+open import Categorical.Ofe.Products
+open import Categorical.Ofe.Exponentials
+open import Categorical.Ofe.Later
+open import Categorical.Ofe.StepIndexed
+open import Categorical.Ofe.Properties
+open import Categorical.Ofe.Predicates
+open import Categorical.Ofe.Predicates.Properties
+open import Categorical.Ofe.Predicates.Closures
+
+-- we specialize here to ofes at universe level zero;
+-- all our types and such fit in there
+Cat = Ofes {lz}{lz}{lz}
+
+open import Categories.Object.Exponential Cat
+open import Categories.Object.Exponentiating Cat binary-products
+open import Categories.Object.BinaryProducts Cat
+open import Categories.Support.SetoidFunctions as SF using () renaming (→-to-⟶ to lift)
+
+open Category Cat
+open BinaryProducts binary-products
+
+data Type : Set where
+  bool : Type
+  int  : Type
+
+data Exp-set : Type → Set where
+  num : ℕ → Exp-set int
+  add : Exp-set int → Exp-set int → Exp-set int
+
+data Val-set : Type → Set where
+  num        : ℕ → Val-set int
+  true false : Val-set bool
+
+-- our values are just the natural numbers
+Val : Type → Setoid lz lz
+Val a = set→setoid (Val-set a)
+
+-- lift expressions to Ofe trivially
+Exp : Type → Obj
+Exp a = Δ⁺ (Exp-set a)
+
+module Elim (A : Type → Obj) where
+
+  Rec = ∀[ Type ] λ a → (Exp a ⇨ A a)
+
+  -- eliminator of the Exp type
+  elim : (Rec ×-ofe (Δ⁺ ℕ)) ⇒ A int →
+         (Rec ×-ofe (Exp int ×-ofe Exp int)) ⇒ A int →
+         ∀ {a} → (Rec ×-ofe (Exp a)) ⇒ A a
+  _⟨$⟩_ (elim f g) (rec , num n) = f ⟨$⟩ (rec , n)
+  _⟨$⟩_ (elim f g) (rec , add e₁ e₂) = g ⟨$⟩ (rec , e₁ , e₂)
+  cong (elim f g) {x = rec , num _} (eq , ≣-refl) = cong f (eq , ≣-refl)
+  cong (elim f g) {x = rec , add _ _} (eq , ≣-refl) = cong g (eq , ≣-refl , ≣-refl)
+
+-- Make the syntax of manipulating exponentiating available
+module _ {X : Obj} where
+  open Exponentiating record { exponential = λ {A} → exp A X } public
+
+Eval = ∀[ Type ] λ a → Exp a ⇨ ⇀ (Val a)
+
+eval-arith : ⊤ ⇒ Eval
+eval-arith =
+  μ
+    (∀[ Type ]-cofe λ a → (Exp a ⇨-cofe (⇀-cofe Val a)))  -- the type of the interpreter is cauchy-complete
+    eval-arith'                                           -- interpreter with guarded recursor
+    (λ a → ⇨-const (⇀-inhabited (Val a)))                 -- initial element
+  where
+
+    -- generalizes the evaluation of an exponent
+    -- to the polymorphic exponent matching Eval.
+    eval' : ∀ {a} → Ofes [ Eval ×-ofe Exp a , ⇀ (Val a) ]
+    eval' {a} = eval ∘ first {C = Exp a} (∀-elim {A = λ a → (Exp a ⇨ (⇀ Val a))} a)
+
+    case-num : (Eval × Δ⁺ ℕ) ⇒ ⇀ (Val int)
+    case-num = fuel (lift num) ∘ π₂ {A = Eval}
+
+    case-add : (Eval × (Exp int × Exp int)) ⇒ ⇀ (Val int)
+    case-add =
+        {!!}                                             -- add values
+      ∘ _⁂_ {C = Eval × Exp int} eval' eval'            -- recursively evaluate the sub-expressions
+      ∘ ×-distrib-× {A = Eval}{B = Exp int}{C = Exp int} -- fiddling with arguments
+
+    eval-arith' : ► Eval ⇒ Eval
+    eval-arith' =
+      ∀-intro (λ a →
+        λ-abs {Γ = ► Eval} (Exp a) (
+            Elim.elim (λ a → ⇀ Val a) case-num case-add
+          ∘ first {A = ► Eval}{B = Eval}{C = Exp a} (
+              ∀-intro (λ a → rec-unfold ∘ ∀-elim a)
+            ∘ ►∀
+          )
+        )
+      )

src/Categorical/Functor/Const.agda

@@ -0,0 +1,14 @@
+module Categorical.Functor.Const where
+
+open import Categories.Category
+open import Categories.Functor using (Functor)
+
+const : ∀ {o ℓ e o' ℓ' e'}{D : Category o' ℓ' e'}{C : Category o ℓ e} → Category.Obj D → Functor C D
+const {D = D} o = record
+  { F₀ = λ _ → o
+  ; F₁ = λ _ → Category.id D
+  ; identity = refl
+  ; homomorphism = λ {X} {Y} {Z} {f} {g} → sym (Category.identityˡ D)
+  ; F-resp-≡ = λ x → refl
+  }
+  where open Category.Equiv D