From 3879860e97500731717939c7a65b2f4b5c886b2e Mon Sep 17 00:00:00 2001 From: Pierre Krafft Date: Thu, 12 Apr 2018 23:04:23 +0200 Subject: [PATCH] More writing --- src/ActorMonad.lagda.tex | 55 +++-- src/Examples/NeedsFrameRule.lagda.tex | 25 +++ src/Examples/Types.lagda.tex | 20 +- src/Membership.lagda.tex | 7 + src/Selective/ActorMonad.lagda.tex | 9 +- src/Selective/ActorMonadNoText.lagda.tex | 208 ++++++++++++++++++ src/Selective/Examples/Call.lagda.tex | 41 +++- .../Examples/CallNoComments.lagda.tex | 111 ++++++++++ 8 files changed, 450 insertions(+), 26 deletions(-) create mode 100644 src/Examples/NeedsFrameRule.lagda.tex create mode 100644 src/Selective/ActorMonadNoText.lagda.tex create mode 100644 src/Selective/Examples/CallNoComments.lagda.tex diff --git a/src/ActorMonad.lagda.tex b/src/ActorMonad.lagda.tex index 9aa28fe..a3c53f6 100644 --- a/src/ActorMonad.lagda.tex +++ b/src/ActorMonad.lagda.tex @@ -80,7 +80,7 @@ Below we have created an instance of an \AgdaRef[ActorMonad]{InboxShape}, showcasing the important concepts. -\AgdaRef[Examples/Types]{TestInbox} is an inbox that can receive two kinds of messages: +\AgdaFunction{TestInbox} is an inbox that can receive two kinds of messages: messages containing a single boolean value, and messages containing a special kind of reference together with a natural number. The reference in the second kind of message can be sent two kinds of messages as well: @@ -109,13 +109,39 @@ if $A <: B$, then every message in $A$ is also a valid message in $B$. Since we model \AgdaRef[ActorMonad]{InboxShape} as a set, the subtype relation can be taken to just be the subset relation. -The drawback of using subsets is that recursive subtypes are not captured, -but we deem it good enough for our purposes and simple to work with. -\todo{Create an example of the type-pollution problem solved} \begin{code} _<:_ = _⊆_ {A = MessageType} \end{code} + +Our representation of subsets uses two datastructures: \AgdaDatatype{∈} and \AgdaDatatype{⊆}. +\AgdaDatatype{∈} is the list or set membership relation, +which we model as a Peano number that tells at what position the element occurs in the list. +An element that appears at the head of a list is at index \AgdaInductiveConstructor{Z}, +and an element that appears somewhere in the tail of the list is +reached by succeeding (\AgdaInductiveConstructor{S}) into the tail of the list. + +\AgdaCatch{Membership}{ElementIn} + +The subset relation \AgdaBound{A} \AgdaDatatype{⊆} \AgdaBound{B} holds if +every member of \AgdaBound{A} is also a member of \AgdaBound{B}. +This can be modelled as a function from indices of \AgdaBound{A} to indices of \AgdaBound{B}, +but this turned out to be inconvenient for our purposes. +An alternative approach is to build subsets as a \emph{view} \parencite{DBLP:journals/jfp/McBrideM04, norell2008dependently} +of the lists in question. +A view is a datatype that reveals something interesting about its indices, \eg that a list is a subset of another. +To define \AgdaDatatype{⊆} we state that the empty list (\AgdaInductiveConstructor{[]}) is a subset of all lists, +and we state that to you can add an element to a subset (\AgdaInductiveConstructor{∷}) if you +are able to prove that the element is a member of the other set. + +\AgdaCatch{Membership}{Subset} + +The drawback of using subsets is that recursive subtypes are not captured, +but we deem it good enough for our purposes and simple to work with. +Proving that \AgdaBound{A} \AgdaFunction{<:} \AgdaBound{B} boils down to +providing an index into \AgdaBound{B} for every element in \AgdaBound{A}. + +\AgdaCatch{Examples/Types}{Subtyping} % %<*ActorPrecondition> @@ -151,9 +177,9 @@ Maintaining the references manually in the model is enough for guaranteeing that references are valid, type correct, and unforgeable. -We type check references just how one would type check variables in any lambda calculus, -\ie by maintaining a variable typing context. -This is commonly done by associating unique variable names to types. +We type check references in the standard way of maintaining a variable typing context. +A typing context associates variables to types, +where variables are commonly referred to by their name. Variable names makes expressions easy to understand for humans, but pose two annoying problems: α-renaming and α-equivalence. α-equivalence is a form of equivalence that captures the intuition that the particular choice of @@ -185,8 +211,8 @@ \end{table} What makes de Bruijn indices easy to work with in Agda is that it lets us manage -the variable typing context as a list of types, with variables / de Bruijn indices being -indices into that list. +the variable typing context as a list of types, with variables as +(de Bruijn) indices into that list. We choose to represent the indices as the membership proposition in order to make the de Bruijn indices correct by construction. This let's us define the type judgement $Γ ⊢ T$ as: @@ -332,20 +358,19 @@ Actors are potentially infinite processes, making it suitable to model \ourlang using coinduction. Following the lead of \textcite{DBLP:journals/corr/AbelC14}, -we represent the monad \AgdaRef[ActorMonad]{ActorM} as a mutual definition of an inductive +we represent the monad \AgdaDatatype{ActorM} as a mutual definition of an inductive datatype and a coinductive record. The record \AgdaRef[ActorMonad]{∞ActorM} is a coalgebra that one interacts with by using its single observation (copattern) \AgdaRef[ActorMonad]{force}. -\AgdaRef[ActorMonad]{force} gives us an element of the \AgdaRef[ActorMonad]{ActorM} datatype +\AgdaRef[ActorMonad]{force} gives us an element of the \AgdaDatatype{ActorM} datatype on which we can pattern match to see which computation to perform next. -Both \AgdaRef[ActorMonad]{ActorM} and \AgdaRef[ActorMonad]{∞ActorM} are indexed by a size $i$. +Both \AgdaDatatype{ActorM} and \AgdaRef[ActorMonad]{∞ActorM} are indexed by a size $i$. The size is a lower bound on on the number of times we can iteratively \AgdaRef[ActorMonad]{force} the computation, but should primarily be seen as a means to establish productivity of recursive definitions. When we actually simulate running actors, -we only care for \AgdaRef[ActorMonad]{ActorM} \AgdaPostulate{∞} \AgdaDatatype{A} -of infinite depth. +we only care for \AgdaDatatype{ActorM} \AgdaPostulate{∞} \AgdaDatatype{A} of infinite depth. \AgdaTarget{ActorM} \AgdaTarget{∞ActorM} @@ -436,7 +461,7 @@ A key concept in Erlang-style actors is that actors can easily get a reference to themselves. For example, in order to implement callbacks the initiating actor must include a reference to themselves for the corresponding actor to reply to. -In \AgdaRef[ActorMonad]{ActorM}, this need is fulfilled by the \AgdaRef[ActorMonad]{Self} construct, +In \AgdaDatatype{ActorM}, this need is fulfilled by the \AgdaRef[ActorMonad]{Self} construct, which adds a reference to the actor itself to the variable context. \AgdaTarget{Self} \begin{code} diff --git a/src/Examples/NeedsFrameRule.lagda.tex b/src/Examples/NeedsFrameRule.lagda.tex new file mode 100644 index 0000000..6ea8b0d --- /dev/null +++ b/src/Examples/NeedsFrameRule.lagda.tex @@ -0,0 +1,25 @@ +\begin{code} +module Examples.NeedsFrameRule where +open import ActorMonad +open import Data.Nat using (ℕ) +open import Membership using (_∈_ ; Z) +open import Data.List using (List ; [] ; _∷_ ; _++_) +open import Data.List.All using (All ; [] ; _∷_) +open import Size using (Size ; Size<_ ; ↑_) +open import Level using (Lift ; lift) + +\end{code} +%<*send-nat> +\begin{code} +send-nat : ∀ {i IS ToIS pre} → + (canSendTo : ToIS ∈ pre) → + ((ValueType ℕ ∷ []) ∈ ToIS) → + ∞ActorM (↑ i) IS ⊤₁ pre (λ _ → pre) +send-nat canSendTo p = canSendTo ![t: p ] (lift 42 ∷ []) + +send-nat-frame : ∀ {i IS ToIS} → + ((ValueType ℕ ∷ []) ∈ ToIS) → + ∞ActorM (↑ i) IS ⊤₁ (ToIS ∷ []) (λ _ → ToIS ∷ []) +send-nat-frame p = Z ![t: p ] (lift 42 ∷ []) +\end{code} +% diff --git a/src/Examples/Types.lagda.tex b/src/Examples/Types.lagda.tex index 3bf9a41..2292ddf 100644 --- a/src/Examples/Types.lagda.tex +++ b/src/Examples/Types.lagda.tex @@ -8,6 +8,7 @@ open import Data.List using (List ; [] ; _∷_) open import Data.String using (String) open import ActorMonad +open import Membership using (_⊆_ ; _∷_ ; [] ; S ; Z) \end{code} @@ -53,20 +54,29 @@ % %<*ExampleInbox> -\AgdaTarget{TestInbox} \begin{code} TestInbox : InboxShape -TestInbox = (ValueType Bool ∷ []) - ∷ ( ReferenceType ( +TestInbox = ( ReferenceType ( (ValueType String ∷ []) ∷ (ValueType Bool ∷ []) ∷ []) ∷ ValueType ℕ ∷ []) + ∷ (ValueType Bool ∷ []) ∷ [] \end{code} % +%<*Subtyping> +\begin{code} +Boolbox : InboxShape +Boolbox = (ValueType Bool ∷ []) + ∷ [] + +test-subtyping : Boolbox <: TestInbox +test-subtyping = (S Z) ∷ [] +\end{code} +% %<*PartialFunction> \begin{code} partial : (n : ℕ) → (n ≡ 2) → Bool @@ -80,14 +90,14 @@ %<*Identity> \begin{code} identity : (A : Set) → A → A -identity A x = x +identity A v = v \end{code} % %<*ImplicitIdentity> \begin{code} identity' : {A : Set} → A → A -identity' x = x +identity' v = v f : ℕ → ℕ f = identity' diff --git a/src/Membership.lagda.tex b/src/Membership.lagda.tex index ed4baf0..47fc908 100644 --- a/src/Membership.lagda.tex +++ b/src/Membership.lagda.tex @@ -19,9 +19,16 @@ x∈[]-⊥ : ∀ {a} {A : Set a} {x : A} → x ∈ [] → ⊥ x∈[]-⊥ () +\end{code} +%<*Subset> +\begin{code} data _⊆_ {a} {A : Set a} : List A → List A → Set a where [] : ∀ {xs} → [] ⊆ xs _∷_ : ∀ {x xs ys} → x ∈ ys → xs ⊆ ys → (x ∷ xs) ⊆ ys +\end{code} +% +\begin{code} + ⊆-suc : ∀ {a} {A : Set a} {y : A} {xs ys : List A} → xs ⊆ ys → xs ⊆ (y ∷ ys) ⊆-suc [] = [] diff --git a/src/Selective/ActorMonad.lagda.tex b/src/Selective/ActorMonad.lagda.tex index 81a7f47..ec6cfd3 100644 --- a/src/Selective/ActorMonad.lagda.tex +++ b/src/Selective/ActorMonad.lagda.tex @@ -67,7 +67,8 @@ %<*SelectedMessage> \begin{code} -record SelectedMessage {IS : InboxShape} (f : MessageFilter IS) : Set₁ where +record SelectedMessage {IS : InboxShape} + (f : MessageFilter IS) : Set₁ where field msg : Message IS msg-ok : f msg ≡ true @@ -76,9 +77,11 @@ %<*SelectedMessageAddReferences> \begin{code} -add-selected-references : TypingContext → ∀ {IS} {filter : MessageFilter IS} → +add-selected-references : TypingContext → ∀ {IS} + {filter : MessageFilter IS} → SelectedMessage filter → TypingContext -add-selected-references Γ m = add-references Γ (SelectedMessage.msg m) +add-selected-references Γ m = + add-references Γ (SelectedMessage.msg m) \end{code} % \begin{code} diff --git a/src/Selective/ActorMonadNoText.lagda.tex b/src/Selective/ActorMonadNoText.lagda.tex new file mode 100644 index 0000000..399067a --- /dev/null +++ b/src/Selective/ActorMonadNoText.lagda.tex @@ -0,0 +1,208 @@ +\begin{code} +module Selective.ActorMonadNoText where +open import Membership using (_∈_ ; _⊆_ ; ⊆-refl ; Z ; S ; find-∈) + +open import Data.List using (List ; [] ; _∷_ ; _++_) +open import Data.List.All using (All ; [] ; _∷_) +open import Data.Unit using (⊤ ; tt) +open import Data.Bool using (Bool ; true ; false) +open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; sym ; cong ; cong₂ ; trans) + +open import Level using (Lift ; lift ; suc ; zero) +open import Size using (Size ; Size<_ ; ↑_) + +mutual + data MessageField : Set₁ where + ValueType : Set → MessageField + ReferenceType : InboxShape → MessageField + + MessageType = List MessageField + + InboxShape = List MessageType + +_<:_ = _⊆_ {A = MessageType} + +ReferenceTypes = List InboxShape +TypingContext = ReferenceTypes + +_⊢_ : TypingContext → InboxShape → Set₁ +Γ ⊢ T = T ∈ Γ + +record _⊢>:_ (Γ : TypingContext) (requested : InboxShape) : Set₁ where + constructor [_]>:_ + field + {actual} : InboxShape + actual-is-sendable : Γ ⊢ actual + actual-handles-requested : requested <: actual + +send-field-content : TypingContext → MessageField → Set₁ +send-field-content Γ (ValueType A) = Lift A +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 Γ + +receive-field-content : MessageField → Set +receive-field-content (ValueType A) = A +receive-field-content (ReferenceType Fw) = ⊤ + +data Message (To : InboxShape) : Set₁ where + Msg : {MT : MessageType} → MT ∈ To → All receive-field-content MT → Message To + +extract-references : MessageType → ReferenceTypes +extract-references [] = [] +extract-references (ValueType x ∷ mt) = extract-references mt +extract-references (ReferenceType T ∷ mt) = T ∷ extract-references mt + +add-references : ∀ {To} → TypingContext → Message To → TypingContext +add-references Γ (Msg {MT} x x₁) = extract-references MT ++ Γ + +\end{code} +%<*MessageFilter> +\begin{code} +MessageFilter : (IS : InboxShape) → Set₁ +MessageFilter IS = Message IS → Bool +\end{code} +% + +%<*SelectedMessage> +\begin{code} +record SelectedMessage {IS : InboxShape} (f : MessageFilter IS) : Set₁ where + field + msg : Message IS + msg-ok : f msg ≡ true +\end{code} +% + +%<*SelectedMessageAddReferences> +\begin{code} +add-selected-references : TypingContext → ∀ {IS} {filter : MessageFilter IS} → + SelectedMessage filter → TypingContext +add-selected-references Γ m = add-references Γ (SelectedMessage.msg m) +\end{code} +% +\begin{code} + + +⊤₁ : Set₁ +⊤₁ = Lift ⊤ + +infixl 1 _∞>>=_ _>>=_ _∞>>_ _>>_ + +\end{code} +%<*MonadHeader> +\begin{code} +data ActorM (i : Size) (IS : InboxShape) : (A : Set₁) → + (pre : TypingContext) → + (post : A → TypingContext) → + 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 +\end{code} +% +\begin{code} +data ActorM (i : Size) (IS : InboxShape) where +\end{code} +%<*MonadConstructors> +\begin{code} + 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 + Spawn : {NewIS : InboxShape} → {A : Set₁} → ∀ {pre postN} → + ActorM i NewIS A [] postN → + ActorM i IS ⊤₁ pre λ _ → NewIS ∷ pre + Send : ∀ {pre} → {ToIS : InboxShape} → + (canSendTo : pre ⊢ ToIS) → + (msg : SendMessage ToIS pre) → + ActorM i IS ⊤₁ pre (λ _ → pre) + Receive : ∀ {pre} → + ActorM i IS (Message IS) pre (add-references pre) + Self : ∀ {pre} → ActorM i IS ⊤₁ pre (λ _ → IS ∷ pre) + Strengthen : ∀ {ys xs} → (inc : ys ⊆ xs) → + ActorM i IS ⊤₁ xs (λ _ → ys) +\end{code} +% +\begin{code} +-- +-- ========== Helpers for ActorM ========== +-- + +open ∞ActorM public + +-- coinduction helper for Value +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} → ∀ {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 : ∀ {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∞ : ∀ {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:_]_ : ∀ {i IS ToIS pre MT} → + (canSendTo : ToIS ∈ pre) → + (MT ∈ ToIS) → + All (send-field-content pre) MT → + ∞ActorM (↑ i) IS ⊤₁ pre (λ _ → pre) +(canSendTo ![t: p ] fields) .force = Send canSendTo (SendM p fields) + +-- coinduction helper for 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 : ∀ {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} diff --git a/src/Selective/Examples/Call.lagda.tex b/src/Selective/Examples/Call.lagda.tex index 4136696..75eadbb 100644 --- a/src/Selective/Examples/Call.lagda.tex +++ b/src/Selective/Examples/Call.lagda.tex @@ -42,17 +42,52 @@ MessageFilter IS call-select {IS} tag sub which (Msg x fs) = call-select-unwrap tag x fs (translate-⊆ sub which) - -call : ∀ {Γ MtTo MtIn i} {To IS IS' : InboxShape} → +\end{code} +%<*CallSignature> +The first parameters to \AgdaFunction{call}\ are implicit and can be inferred from how they are used. +\AgdaBound{Γ} is the current variable typing context, +\AgdaBound{MtTo} and \AgdaBound{MtIn} denote the optional fields of the outgoing and incoming message, +\AgdaBound{To} is the interface of the callee's reference, +\AgdaBound{IS} is the interface of the current actor, +and \AgdaBound{IS'} is the interface of the reference that will be sent to the callee. +\begin{code} +call : {Γ : TypingContext} {i : Size} + {MtTo MtIn : MessageType} + {To IS IS' : InboxShape} → +\end{code} +The actor that we're calling must exist as a variable. +\begin{code} (Γ ⊢ To) → - ((ValueType UniqueTag ∷ ReferenceType IS' ∷ MtTo) ∈ To) → +\end{code} +The actor that we're calling must accept a message containing the unique tag and a reference. +There are no further constraints on the additional fields \AgdaBound{MtTo}. +\begin{code} + ((ValueType UniqueTag ∷ ReferenceType IS' ∷ MtTo) ∈ To) → +\end{code} +The caller must supply the unique tag manually, but it would be easy to extend the actor monad +with some state that can provide unique tags automatically. +The caller must also supply content for all the additional fields of the message. +\begin{code} (tag : UniqueTag) → All (send-field-content Γ) MtTo → +\end{code} +The reference that is sent to the callee (\AgdaBound{IS'}) must of course +be a subtype of the current actor (\AgdaBound{IS}). +Furthermore, the reference that we're sending must accept messages that contain the unique tag +and the rest of the answer. +\begin{code} (ISsubs : IS' <: IS) → (whichIn : (ValueType UniqueTag ∷ MtIn) ∈ IS') → +\end{code} +Finally, call creates an actor computation that returns the reply and +where the references in the answer are added to the context. +\begin{code} ∞ActorM i IS (SelectedMessage (call-select tag ISsubs whichIn)) Γ (add-selected-references Γ) +\end{code} +% +\begin{code} call {Γ} {IS = IS} var toFi tag vals sub whichIn = \end{code} %<*CallComputation> diff --git a/src/Selective/Examples/CallNoComments.lagda.tex b/src/Selective/Examples/CallNoComments.lagda.tex new file mode 100644 index 0000000..e7c92cc --- /dev/null +++ b/src/Selective/Examples/CallNoComments.lagda.tex @@ -0,0 +1,111 @@ +\begin{code} +module Selective.Examples.CallNoComments where + +open import Selective.ActorMonad public +open import Data.List using (List ; _∷_ ; [] ; _++_) +open import Data.List.All using (All ; _∷_ ; []) +open import Data.Bool using (Bool ; if_then_else_ ; false ; true) +open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _≟_ ) +open import Size +open import Level using (Lift ; lift) renaming (zero to lzero ; suc to lsuc) +open import Data.List.Any using (here ; there) +open import Relation.Binary.PropositionalEquality + using (_≡_ ; refl ; cong ; sym ; inspect ; [_] ; trans) +open import Membership using ( + _∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] + ; ⊆-refl ; ⊆-trans ; ⊆-suc ; translate-⊆ + ) +open import Data.Unit using (⊤ ; tt) +open import Relation.Nullary using (yes ; no) + +open SelectedMessage + +UniqueTag = ℕ + +call-select-unwrap : ∀ {MtIn MT} {IS : InboxShape} → + UniqueTag → + MT ∈ IS → + All receive-field-content MT → + (ValueType UniqueTag ∷ MtIn) ∈ IS → + Bool +call-select-unwrap tag Z (tag' ∷ fs) Z with (tag ≟ tag') +... | yes p = true +... | no p = false +call-select-unwrap _ Z _ (S p) = false +call-select-unwrap _ (S x) _ Z = false +call-select-unwrap tag (S x) fs (S p) = call-select-unwrap tag x fs p + +call-select : ∀ {IS IS' MtIn} → + UniqueTag → + IS' <: IS → + (ValueType UniqueTag ∷ MtIn) ∈ IS' → + MessageFilter IS +call-select {IS} tag sub which (Msg x fs) = + call-select-unwrap tag x fs (translate-⊆ sub which) + +call : {Γ : TypingContext} {i : Size} + {MtTo MtIn : MessageType} + {To IS IS' : InboxShape} → + (Γ ⊢ To) → + ((ValueType UniqueTag ∷ ReferenceType IS' ∷ MtTo) ∈ To) → + (tag : UniqueTag) → + All (send-field-content Γ) MtTo → + (ISsubs : IS' <: IS) → + (whichIn : (ValueType UniqueTag ∷ MtIn) ∈ IS') → + ∞ActorM i IS + (SelectedMessage (call-select tag ISsubs whichIn)) + Γ (add-selected-references Γ) +call {Γ} {IS = IS} var toFi tag vals sub whichIn = + do + self + S var ![t: toFi ] ((lift tag) ∷ ([ Z ]>: sub) ∷ (translate-fields vals)) + strengthen (⊆-suc ⊆-refl) + selective-receive (call-select tag sub whichIn) + where + translate-fields : ∀ {MT} → + All (send-field-content Γ) MT → + All (send-field-content (IS ∷ Γ)) MT + translate-fields [] = [] + translate-fields {ValueType x ∷ MT} (px ∷ vals) = + px ∷ (translate-fields vals) + translate-fields {ReferenceType x ∷ MT} (([ p ]>: v) ∷ vals) = + ([ (S p) ]>: v) ∷ (translate-fields vals) + +Calculator : InboxShape +Calculator = ( + ValueType UniqueTag ∷ + ReferenceType (( + ValueType UniqueTag ∷ + ValueType ℕ ∷ []) ∷ [] + ) ∷ + ValueType ℕ ∷ + ValueType ℕ ∷ [] + ) ∷ [] + +calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → []) +calculatorActor .force = receive ∞>>= λ { + (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) .force → + (Z ![t: Z ] ((lift tag) ∷ (lift (n + m)) ∷ [])) ∞>> (do + strengthen [] + calculatorActor) + ; (Msg (S ()) _) + } + +TestBox : InboxShape +TestBox = ( + ValueType UniqueTag ∷ + ValueType ℕ ∷ []) ∷ + [] ∷ [] + +calltestActor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) +calltestActor .force = spawn∞ calculatorActor ∞>> (do + x ← call Z Z 0 ((lift 10) ∷ ((lift 32) ∷ [])) (Z ∷ []) Z + strengthen [] + return-result x) + where + return-result : SelectedMessage {TestBox} (call-select 0 (Z ∷ []) Z) → + ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → []) + return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n + return-result record { msg = (Msg (S x) x₁) ; msg-ok = () } + +\end{code}