Modern coinduction with sized types

+ bunch of examples

README.md

@@ -10,8 +10,19 @@ in a style inspired by Effects from Idris and Koen Claessen's Poor Man's Concurr
 
 | Dependency       | Version                                  |
 |------------------|------------------------------------------|
-| Agda             | 2.5.3                                    |
-| standard-library | 27182f8b24f0493a184e5ee82b285d18c61d6a37 |
+| Agda             | 8a7ad7f79c09d3a55110b6f92ab07267564601f0 |
+| standard-library | 2a40a031e40042e72e245cce17956e5df49fcdd5 |
+
+## How to build?
+Agda and the standard library are nightlies for Agda 2.5.4.
+The simplest way to build Agda is to clone the repo and run
+`stack install --stack-yaml stack-8.2.2.yaml`.
+The nightlies are used to get do-notation and solve some bugs with codata.
+
+The project itself can be built with make or using agda-mode in emacs.
+Latex files can be generated with `make latex`, but most of the thesis is kept in ShareLatex.
+
+## Project structure
 
 | File                  | Description                                              |
 |-----------------------|----------------------------------------------------------|
@@ -20,4 +31,6 @@ in a style inspired by Effects from Idris and Koen Claessen's Poor Man's Concurr
 | ActorMonad            | The embedding you use to create different actor programs |
 | SimulationEnvironment | The datastructures and proofs used in the simulation     |
 | EnvironmentOperations | Functions modifying the simulation environment           |
+| Examples              | Showcases patterns and code used in the thesis           |
+| Selective             | Selective receive as a primary operation                 |
 | unused                | Old code I didn't want to throw away yet                 |

latex.make

@@ -4,6 +4,8 @@ subdirs := src/ src/Examples/ src/Selective/ src/Selective/Examples/
 sources := $(wildcard $(subdirs:%=%*.lagda.tex))
 renamed := $(sources:%.lagda.tex=%.tex)
 moved   := $(renamed:src/%=$(LATEX-OUTPUT-DIR)%)
+out-subdirs := $(subdirs:src/%=$(LATEX-OUTPUT-DIR)%)
+generated   :=  $(wildcard $(out-subdirs:%=%*.tex))
 
 $(moved): $(LATEX-OUTPUT-DIR)%.tex: src/%.lagda.tex
 	stack exec agda -- --latex-dir=$(LATEX-OUTPUT-DIR) --latex $<
@@ -12,4 +14,5 @@ $(moved): $(LATEX-OUTPUT-DIR)%.tex: src/%.lagda.tex
 
 .PHONY: all clean
 all: $(moved)
-clean: rm -rf $(LATEX-OUTPUT-DIR)
+clean:
+	rm $(wildcard $(wildcard $(generated)))

src/ActorMonad.lagda.tex

@@ -6,8 +6,8 @@
 open import Data.List.All using (All ; [] ; _∷_)
 open import Data.Unit using (⊤ ; tt)
 
-open import Coinduction using (∞ ; ♯_ ; ♭)
 open import Level using (Lift ; lift ; suc ; zero)
+open import Size using (Size ; Size<_ ; ↑_)
 \end{code}
 
 An Actor is indexed by the shape of its inbox.
@@ -177,13 +177,13 @@
 Following are some examples comparing a λ-calculus with names
 and a λ-calculus using de Bruijn indices.
 
-\begin{table}[]
+\begin{table}[h]
 \centering
 \begin{tabular}{ll}
 Named                                 & de Bruijn                 \\
 $ λ\ x → x $                          & $ λ\ 1 $                  \\
 $ λ\ x → λ\ y → x $                   & $ λ\ λ\ 2 $               \\
-$ λ\ x → λ\ y → λ\ z → x\ z\ (y\ z) $ & $ λ\ λ\ λ\ 3\ 1\ (2\ 1) $ \\         
+$ λ\ x → λ\ y → λ\ z → x\ z\ (y\ z) $ & $ λ\ λ\ λ\ 3\ 1\ (2\ 1) $ \\
 \end{tabular}
 \end{table}
 
@@ -255,7 +255,10 @@
 send-field-content Γ (ReferenceType requested) = Γ ⊢>: requested
 
 data SendMessage (To : InboxShape) (Γ : TypingContext) : Set₁ where
-  SendM : {MT : MessageType} → MT ∈ To → All (send-field-content Γ) MT → SendMessage To Γ
+  SendM : {MT : MessageType} →
+          MT ∈ To →
+          All (send-field-content Γ) MT →
+          SendMessage To Γ
 \end{code}
 
 Somewhat surprisingly,
@@ -275,7 +278,10 @@
 receive-field-content (ReferenceType Fw) = ⊤
 
 data Message (To : InboxShape) : Set₁ where
-  Msg : {MT : MessageType} → MT ∈ To → All receive-field-content MT → Message To
+  Msg : {MT : MessageType} →
+        MT ∈ To →
+        All receive-field-content MT →
+        Message To
 
 extract-references : MessageType → ReferenceTypes
 extract-references [] = []
@@ -287,7 +293,7 @@
 \end{code}
 %</Messages>
 \begin{code}
-infixl 1 _>>=_
+infixl 1 _∞>>=_ _>>=_ _∞>>_ _>>_
 \end{code}
 %<*LiftTop>
 \AgdaTarget{⊤₁}
@@ -322,10 +328,20 @@
 
 \AgdaTarget{ActorM}
 \begin{code}
-data ActorM (IS : InboxShape) : (A : Set₁) →
+data ActorM (i : Size) (IS : InboxShape) : (A : Set₁) →
               (pre : TypingContext) →
               (post : A → TypingContext) →
-              Set₂ where
+              Set₂
+
+record ∞ActorM (i : Size) (IS : InboxShape) (A : Set₁)
+               (pre : TypingContext)
+               (post : A → TypingContext) :
+               Set₂ where
+  coinductive
+  constructor delay_
+  field force : ∀ {j : Size< i} → ActorM j IS A pre post
+
+data ActorM (i : Size) (IS : InboxShape) where
 \end{code}
 %</ActorMonad>
 %<*ActorMonadBindReturn>
@@ -344,10 +360,10 @@
 
 \AgdaTarget{Return}
 \begin{code}
-  Return : ∀ {A post} → (val : A) → ActorM IS A (post val) post
-  _>>=_ : ∀ {A B pre mid post} → (m : ∞ (ActorM IS A pre mid)) →
-    (f : (x : A) → ∞ (ActorM IS B (mid x) (post))) →
-    ActorM IS B pre post
+  Return : ∀ {A post} → (val : A) → ActorM i IS A (post val) post
+  _∞>>=_ : ∀ {A B pre mid post} → (m : ∞ActorM i IS A pre mid) →
+    (f : (x : A) → ∞ActorM i IS B (mid x) (post)) →
+    ActorM i IS B pre post
 \end{code}
 %</ActorMonadBindReturn>
 %<*ActorMonadSpawn>
@@ -359,13 +375,13 @@
 \AgdaTarget{Spawn}
 \begin{code}
   Spawn : {NewIS : InboxShape} → {A : Set₁} → ∀ {pre postN} →
-    ActorM NewIS A [] postN →
-    ActorM IS ⊤₁ pre λ _ → NewIS ∷ pre
+    ActorM i NewIS A [] postN →
+    ActorM i IS ⊤₁ pre λ _ → NewIS ∷ pre
 \end{code}
 %</ActorMonadSpawn>
 %<*ActorMonadSend>
 An actor can send messages to any actor it has a reference to.
-It is not explicit in the monad what happens to a sent message, but we will see in (SECTION) 
+It is not explicit in the monad what happens to a sent message, but we will see in (SECTION)
 that evaluating Send will append the message to the actor being referenced.
 The reference variable might be a subtype to the underlying actor it references,
 but this fact is completely opaque to the \AgdaRef[ActorMonad]{Send} construct.
@@ -377,7 +393,7 @@
   Send : ∀ {pre} → {ToIS : InboxShape} →
     (canSendTo : pre ⊢ ToIS) →
     (msg : SendMessage ToIS pre) →
-    ActorM IS ⊤₁ pre (λ _ → pre)
+    ActorM i IS ⊤₁ pre (λ _ → pre)
 \end{code}
 %</ActorMonadSend>
 %<*ActorMonadReceive>
@@ -392,7 +408,7 @@
 actors to be implemented as non-parameterized monads.
 \AgdaTarget{Receive}
 \begin{code}
-  Receive : ∀ {pre} → ActorM IS (Message IS) pre (add-references pre)
+  Receive : ∀ {pre} → ActorM i IS (Message IS) pre (add-references pre)
 \end{code}
 %</ActorMonadReceive>
 %<*ActorMonadSelf>
@@ -402,7 +418,7 @@
 In \AgdaRef[ActorMonad]{ActorM}, this need is fulfilled by the \AgdaRef[ActorMonad]{Self} construct,
 which adds a reference to the actor itself to the variable context.
 \begin{code}
-  Self : ∀ {pre} → ActorM IS ⊤₁ pre (λ _ → IS ∷ pre)
+  Self : ∀ {pre} → ActorM i IS ⊤₁ pre (λ _ → IS ∷ pre)
 \end{code}
 %</ActorMonadSelf>
 %<*ActorMonadStrengthen>
@@ -423,7 +439,7 @@
 \AgdaTarget{Strengthen}
 \begin{code}
   Strengthen   : ∀ {ys xs} → (inc : ys ⊆ xs) →
-    ActorM IS ⊤₁ xs (λ _ → ys)
+    ActorM i IS ⊤₁ xs (λ _ → ys)
 \end{code}
 %</ActorMonadStrengthen>
 
@@ -434,44 +450,79 @@
 -- ========== Helpers for ActorM ==========
 --
 
+open ∞ActorM public
+
 -- coinduction helper for Value
-return₁ : {A : Set (suc zero)} → ∀ {IS post} → (val : A) → ∞ (ActorM IS A (post val) post)
-return₁ val = ♯ Return val
+return₁ : {A : Set (suc zero)} → ∀ {i IS post} → (val : A) →
+          ∞ActorM i IS A (post val) post
+return₁ val .force = Return val
 
 -- universe lifting for return₁
-return : {A : Set} → ∀ {IS post} → (val : A) → ∞ (ActorM IS (Lift A) (post (lift val)) post)
+return : {A : Set} → ∀ {i IS post} → (val : A) →
+         ∞ActorM i IS (Lift A) (post (lift val)) post
 return val = return₁ (lift val)
 
+_>>=_ : ∀ {i IS A B pre mid post} → (m : ∞ActorM i IS A pre mid) →
+  (f : (x : A) → ∞ActorM i IS B (mid x) (post)) →
+  ∞ActorM i IS B pre post
+(m >>= f) .force = m ∞>>= f
+
+_∞>>_ : ∀ {i IS A B pre mid post} → (m : ∞ActorM i IS A pre (λ _ → mid)) →
+  (n : ∞ActorM i IS B mid post) →
+  ActorM i IS B pre post
+m ∞>> n = m ∞>>= λ _ → n
+
+[mid:_]_>>=_ : ∀ {i IS A B pre post} → ∀ mid →
+  (m : ∞ActorM i IS A pre mid) →
+  (f : (x : A) → ∞ActorM i IS B (mid x) (post)) →
+  ∞ActorM i IS B pre post
+[mid: mid ] m >>= f = _>>=_ {mid = mid} m f
+
+_>>_ : ∀ {i IS A B pre mid post} → (m : ∞ActorM i IS A pre (λ _ → mid)) →
+  (n : ∞ActorM i IS B mid post) →
+  ∞ActorM i IS B pre post
+(m >> n) .force = m ∞>> n
+
+[mid:_]_>>_ : ∀ {i IS A B pre post} → ∀ mid →
+  (m : ∞ActorM i IS A pre (λ _ → mid)) →
+  (n : ∞ActorM i IS B mid (post)) →
+  ∞ActorM i IS B pre post
+[mid: mid ] m >> f = _>>_ {mid = mid} m f
+
 -- coinduction helper for spawn
-spawn : ∀ {IS NewIS A pre postN} →
-  ActorM NewIS A [] postN →
-  ∞ (ActorM IS ⊤₁ pre λ _ → NewIS ∷ pre)
-spawn newAct = ♯ Spawn newAct
+spawn : ∀ {i IS NewIS A pre postN} →
+  ActorM i NewIS A [] postN →
+  ∞ActorM (↑ i) IS ⊤₁ pre λ _ → NewIS ∷ pre
+spawn newAct .force = Spawn newAct
 
 -- spawn potentially infinite actors
-spawn∞ : ∀ {IS NewIS A pre postN} →
-  ∞ (ActorM NewIS A [] postN) →
-  ∞ (ActorM IS ⊤₁ pre λ _ → NewIS ∷ pre)
-spawn∞ newAct = spawn (♭ newAct)
+spawn∞ : ∀ {i IS NewIS A pre postN} →
+  ∞ActorM (↑ i) NewIS A [] postN →
+  ∞ActorM (↑ i) IS ⊤₁ pre λ _ → NewIS ∷ pre
+spawn∞ newAct = spawn (newAct .force)
 
 -- coinduction helper and neater syntax for message sending
-_![t:_]_ : ∀ {IS ToIS pre MT} →
+_![t:_]_ : ∀ {i IS ToIS pre MT} →
   (canSendTo : ToIS ∈ pre) →
   (MT ∈ ToIS) →
   All (send-field-content pre) MT →
-  ∞ (ActorM IS ⊤₁ pre (λ _ → pre))
-canSendTo ![t: p ] fields = ♯ Send canSendTo (SendM p fields)
+  ∞ActorM i IS ⊤₁ pre (λ _ → pre)
+(canSendTo ![t: p ] fields) .force = Send canSendTo (SendM p fields)
 
 -- coinduction helper for Receive
-receive : ∀ {IS pre} → ∞ (ActorM IS (Message IS) pre (add-references pre))
-receive = ♯ Receive
+receive : ∀ {i IS pre} → ∞ActorM i IS (Message IS) pre (add-references pre)
+receive .force = Receive
+
+self : ∀ {i IS pre} → ∞ActorM i IS ⊤₁ pre (λ _ → IS ∷ pre)
+self .force = Self
 
 -- coinduction helper for Strengthen
-strengthen : ∀ {IS xs ys} → ys ⊆ xs → ∞ (ActorM IS ⊤₁ xs (λ _ → ys))
-strengthen inc = ♯ Strengthen inc
+strengthen : ∀ {i IS xs ys} → ys ⊆ xs → ∞ActorM i IS ⊤₁ xs (λ _ → ys)
+strengthen inc .force = Strengthen inc
 
 ⊠-of-values : List Set → InboxShape
 ⊠-of-values [] = []
 ⊠-of-values (x ∷ vs) = (ValueType x ∷ []) ∷ ⊠-of-values vs
 \end{code}
-%</ActorMonadHelpers>
+%</ActorMonadHelpers>
+

src/Colist.agda

@@ -0,0 +1,14 @@
+module Colist where
+
+open import Size using (Size ; Size<_)
+
+data Colist (i : Size) {a} (A : Set a) : Set a
+
+record ∞Colist (i : Size) {a} (A : Set a) : Set a where
+  coinductive
+  constructor delay_
+  field force : ∀ {j : Size< i} → Colist i A
+
+data Colist (i : Size) {a} (A : Set a) where
+  [] : Colist i A
+  _∷_ : (x : A) (xs : ∞Colist i A) → Colist i A

src/EnvironmentOperations.agda

@@ -18,6 +18,7 @@ open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; co
 open import Relation.Nullary using (Dec ; yes ; no)
 
 open import Level using (Lift ; lift)
+open import Size using (∞)
 
 open Actor
 open ValidActor
@@ -26,7 +27,7 @@ open NamedInbox
 
 -- We can create a new Actor from an ActorM if we know its name.
 -- This is used when spawning an actor.
-new-actor : ∀ {IS A post} → ActorM IS A [] post → Name → Actor
+new-actor : ∀ {IS A post} → ActorM ∞ IS A [] post → Name → Actor
 new-actor {IS} {A} {post} m name = record
                                         { inbox-shape = IS
                                         ; A = A
@@ -41,7 +42,7 @@ new-actor {IS} {A} {post} m name = record
 -- An actor can be lifted to run sub-programs that need less references
 lift-actor : (actor : Actor) → {pre : TypingContext} → (references : Store) →
               (pre-eq-refs : (map shape references) ≡ pre) →
-              ActorM (inbox-shape actor) (A actor) pre (post actor) → Actor
+              ActorM ∞ (inbox-shape actor) (A actor) pre (post actor) → Actor
 lift-actor actor {pre} references pre-eq-refs m = record
                                               { inbox-shape = inbox-shape actor
                                               ; A = A actor
@@ -55,7 +56,7 @@ lift-actor actor {pre} references pre-eq-refs m = record
 
 -- Replace the monadic part of an actor
 -- Many of the bind-operations don't change anything except what the next step should be.
-replace-actorM : (actor : Actor) → ActorM (inbox-shape actor) (A actor) (pre actor) (post actor) → Actor
+replace-actorM : (actor : Actor) → ActorM ∞ (inbox-shape actor) (A actor) (pre actor) (post actor) → Actor
 replace-actorM actor m = record
                            { inbox-shape = inbox-shape actor
                            ; A = A actor
@@ -70,7 +71,7 @@ replace-actorM actor m = record
 -- Add one reference to an actor.
 -- Used when receiving a reference, spawn, or self.
 -- The precondition and references are equal via the congruence relation on consing the shape of the reference.
-add-reference : (actor : Actor) → (nm : NamedInbox) → ActorM (inbox-shape actor) (A actor) (shape nm ∷ pre actor) (post actor) → Actor
+add-reference : (actor : Actor) → (nm : NamedInbox) → ActorM ∞ (inbox-shape actor) (A actor) (shape nm ∷ pre actor) (post actor) → Actor
 add-reference actor nm m = record
                              { inbox-shape = inbox-shape actor
                              ; A = A actor
@@ -82,7 +83,7 @@ add-reference actor nm m = record
                              ; name = name actor
                              }
 
-add-references-to-actor : (actor : Actor) → (nms : List NamedInbox) → ActorM (inbox-shape actor) (A actor) ((map shape nms) ++ pre actor) (post actor) → Actor
+add-references-to-actor : (actor : Actor) → (nms : List NamedInbox) → ActorM ∞ (inbox-shape actor) (A actor) ((map shape nms) ++ pre actor) (post actor) → Actor
 add-references-to-actor actor nms m = record
                                         { inbox-shape = inbox-shape actor
                                         ; A = A actor
@@ -94,7 +95,10 @@ add-references-to-actor actor nms m = record
                                         ; name = name actor
                                         }
 
-add-references-rewrite : (actor : Actor) → (nms : List NamedInbox) → {x : Message (inbox-shape actor)} → map shape nms ++ pre actor ≡ add-references (pre actor) x → ActorM (inbox-shape actor) (A actor) (add-references (pre actor) x) (post actor) → Actor
+add-references-rewrite : (actor : Actor) → (nms : List NamedInbox) → {x : Message (inbox-shape actor)} →
+  map shape nms ++ pre actor ≡ add-references (pre actor) x →
+  ActorM ∞ (inbox-shape actor) (A actor) (add-references (pre actor) x) (post actor) →
+  Actor
 add-references-rewrite actor nms {x} p m = record
                              { inbox-shape = inbox-shape actor
                              ; A = A actor
@@ -243,7 +247,7 @@ messages-valid-suc {store} {IS} {n} {x} {nx ∷ _} frsh (px ∷ vi) = message-va
 
 -- Add a new actor to the environment.
 -- The actor is added to the top of the list of actors.
-add-top : ∀ {IS A post} → ActorM IS A [] post → Env → Env
+add-top : ∀ {IS A post} → ActorM ∞ IS A [] post → Env → Env
 add-top {IS} {A} {post} actor-m env = record
                                  { acts = record
                                             { inbox-shape = IS