diff --git a/src/ActorMonad.lagda.tex b/src/ActorMonad.lagda.tex index 4e99fa0..4cecef2 100644 --- a/src/ActorMonad.lagda.tex +++ b/src/ActorMonad.lagda.tex @@ -135,37 +135,31 @@ % %<*ActorPrecondition> -It is crucial that actor references are completely unforgeable if type safety is to be preserved. -If an actor is allowed to manufacture references on its own, -every guarantee we have about message types becomes invalid and unusable. -Allowing either the name or the type of a reference to be controlled in user space -makes it possible to create a reference to an inbox that is incompatible with the underlying inbox, -making it possible to send messages that will not be understood by the receiver. - -In other settings we could simply have hidden the constructor of actor references, -i.e. by moving it to an internal module or marking it as abstract. -That tactic is simple and pragmatic, -but does not work in a formal setting like Agda without using postulates. -This posed a difficult problem in our implementation -since we realized that we would need to make a major diversion from how -references are handled by \textcite{DBLP:conf/ecoop/FowlerLW17}. - -When \textcite{DBLP:conf/ecoop/FowlerLW17} type terms, -values and references are treated the same way. -Since our model is an embedding in Agda, -this would mean that both references and values are normal Agda terms. -Initially we tried to follow this route by modelling references as a name tagged with a type. +A reference to an actor is a name that is used to look up that actor's inbox in order to write or read from it. +We assign types to references in order to statically guarantee that we will only send messages to an inbox which the receiving actor can understand. +The property to maintain for this to hold is that the type of the reference must be a subtype of the inbox it references: + +\[ + \begin{array}{@{}c@{}} + S <: T \quad inbox : \overrightarrow{T} \quad name \mapsto inbox \\ + \hline + \operatorname{Reference}(name) : S +\end{array} +\] + +The desire to statically check that references are well-typed has affected the design of \ourlang a lot. +We first tried an encoding of references where a name is simply tagged with a type: \AgdaCatch{Examples/Types}{ActorRef} -One quickly realizes that this data-type is easily forged and, as said, -hiding the constructor is not a good enough option. -We also realized that it would not be possible to maintain any proofs of references being valid -if we went this route, a problem related to how we incorporate Agda functions in the syntax. -The solution that seemed to fit best in the setting of Agda -is to treat references separately from values. +This encoding is intuitive and simple, but it does not capture $S <: T$, nor does it capture $name \mapsto inbox$. +Using this encoding thus requires finding a way to maintain additional proofs. + +To maintain the necessary proofs of references being valid requires that we encode more things in the type system. +The solution that seem to fit best in the setting of Agda is to make a bigger distinction between references and values. Values are kept as normal Agda terms, only restricted under Agda's usual typing rules. -References, on the other hand, are treated as variables that are maintained explicitly in the model. -Maintaining the references manually in the model is enough for guaranteeing that references -are valid, type correct, and unforgeable. +References, on the other hand, are treated as variables that are maintained explicitly in the model, +encoded in the type parameter of each actor. +This technique makes it possible to maintain type correctness of references, +as long as the effect every actor operation has on the reference variables is carefully designed. We type check references in the standard way of maintaining a variable typing context. A typing context associates variables to types, @@ -219,7 +213,7 @@ % %<*ReferenceSubtype> -For inboxes the subtype relation $A <: B$ says that +For inboxes, the subtype relation $A <: B$ says that every message in $A$ is also a valid message in $B$. It should therefore be possible to downcast a reference of type $B$ to a reference of type $A$, since every message sent to a reference of type $A$ will be a valid message in $B$. @@ -263,7 +257,7 @@ For references, the instantiation is not a simple Agda term, but rather a variable in the reference context. The type of the selected reference variable must be compatible with the type that the receiver expects, -\ie the types have to have the correct subtype relation. +\ie they must have the correct subtype relation. \begin{code} @@ -385,7 +379,7 @@ monad, which is explained in section \ref{parameterized_monads}. Bind chains together potentially infinite sub-computations, and we can see that bind preserves the size (observation depth) $i$. -Agda implements a sort of subtyping for sizes, +Agda implements subtyping for sizes, so computations of different sizes can still be composed via bind. We don't give the constructors \AgdaInductiveConstructor{Return} diff --git a/src/Examples/Types.lagda.tex b/src/Examples/Types.lagda.tex index efd79f4..965542d 100644 --- a/src/Examples/Types.lagda.tex +++ b/src/Examples/Types.lagda.tex @@ -50,8 +50,10 @@ \end{code} %<*ActorRef> \begin{code} -data ActorRef : (InboxType : Set) → Set where - create-actor-ref : ∀ {A} → Name → ActorRef A +record ActorRef (InboxType : Set) : Set where + constructor create-actor-ref + field + name : Name \end{code} % diff --git a/src/Selective/Examples/CallNoComments.lagda.tex b/src/Selective/Examples/CallNoComments.lagda.tex index dc9ead3..70b4d44 100644 --- a/src/Selective/Examples/CallNoComments.lagda.tex +++ b/src/Selective/Examples/CallNoComments.lagda.tex @@ -1,5 +1,5 @@ \begin{code} -module Selective.Examples.Call where +module Selective.Examples.CallNoComments where open import Selective.ActorMonad open import Prelude