From 057202deb55fd00504b197ccaf3c3afe115d3204 Mon Sep 17 00:00:00 2001 From: Pierre Krafft Date: Tue, 12 Jun 2018 16:43:28 +0200 Subject: [PATCH] Writing --- src/ActorMonad.lagda.tex | 25 +++++++++++++++-------- src/Examples/MonadParameterized.lagda.tex | 17 ++++++++------- src/Examples/Types.lagda.tex | 10 +++++---- 3 files changed, 32 insertions(+), 20 deletions(-) diff --git a/src/ActorMonad.lagda.tex b/src/ActorMonad.lagda.tex index 468f626..563befb 100644 --- a/src/ActorMonad.lagda.tex +++ b/src/ActorMonad.lagda.tex @@ -81,14 +81,16 @@ messages containing a single boolean value, and messages containing a single string value. -\AgdaCatchGroup{Examples/Types}{ExampleInbox} +\AgdaCatchGroup{Examples/Types}{ExampleMessages} + +\AgdaCatchGroup{Examples/Types}{TestInbox} % %<*InboxShapeSubtype> The Interface Segregation Principle (ISP) is a design principle that states -that no client should be forced to depend on methods it does not use \parencite{martin2002agile}. -\textcite{martin2002agile} claims that when clients depend upon objects which -contain methods used only by other clients, this can lead to fragile code. +that no client should be forced to depend on methods it does not use; +when clients depend upon objects which contain methods used only by other clients, +this can lead to fragile code~\parencite{martin2002agile}. In particular, if a client depends on an interface that contains methods that the client does not use but others do, that client will be affected by changes that those other clients force on the interface. @@ -132,8 +134,12 @@ 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 +Proving that \mbox{\AgdaBound{A} \AgdaFunction{<:} \AgdaBound{B}} boils down to providing an index into \AgdaBound{B} for every element in \AgdaBound{A}. +For example, \AgdaFunction{text{-}subtyping} proves that an inbox that only accepts +\AgdaFunction{BoolMessage} is a subtype of the \AgdaFunction{TestInbox} from before. + +\AgdaCatchGroup{Examples/Types}{TestInbox} \AgdaCatchGroup{Examples/Types}{Subtyping} % @@ -165,11 +171,10 @@ 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. +but pose two annoying problems: α-equivalence and α-renaming. α-equivalence is a form of equivalence that captures the intuition that the particular choice of a bound variable name does not usually matter \parencite{turbak2008design}. - Renaming the variables of an expression in a way that preserves α-equivalence is called α-renaming \parencite{turbak2008design}. α-renaming is a part of the general concept of substitution, @@ -183,7 +188,7 @@ A de Bruijn index is a natural number that represents an occurrence of a variable in a λ-term, and denotes the number of binders that are in scope between that occurrence and its corresponding binder. -Figure~\ref{fig:debruijn} shows some examples comparing a λ-calculus with names +Table~\ref{tab:debruijn} shows some examples comparing a λ-calculus with names to a λ-calculus using de Bruijn indices. \input{include/figures/debruijn} @@ -289,7 +294,9 @@ making it easy to create indices into the variable context without making them a part of the message. It would be possible to make the reference field content be an index into the variable context, -but it would make the model slightly more complicated without making it more powerful. +but it would make the model slightly more complicated without making it more powerful; +the programmer can already create indices when they are needed and, since the typing context +is constantly changing, a specific index is often not valid for long. \begin{minipage}{\textwidth} \begin{code} diff --git a/src/Examples/MonadParameterized.lagda.tex b/src/Examples/MonadParameterized.lagda.tex index a5dd4e1..bbd702d 100644 --- a/src/Examples/MonadParameterized.lagda.tex +++ b/src/Examples/MonadParameterized.lagda.tex @@ -13,7 +13,7 @@ \begin{code} data MonadParam' (B : Set) : {p q : Set} → p → q → Set₁ where return : ∀ {p} → {pre : p} → B → MonadParam' B pre pre - _>>=_ : ∀ {A X Y Z} → {pre : X} → {mid : Y} → {post : Z} → + _>>=_ : ∀ {A X Y Z} → {pre : X} → {mid : Y} → {post : Z} → MonadParam' A pre mid → (A → MonadParam' B mid post) → MonadParam' B pre post @@ -23,12 +23,15 @@ %<*Monad> \begin{code} data MonadParam (B : Set) : {p q : Set} → p → (B → q) → Set₁ where - return : {S : Set} → {post : B → S} → (val : B) → - MonadParam B (post val) post - _>>=_ : ∀ {A X Y Z} → {pre : X} → {mid : A → Y} → {post : B → Z} → - MonadParam A pre mid → - ((x : A) → MonadParam B (mid x) post) → - MonadParam B pre post + return : {S : Set} → {post : B → S} → + (val : B) → + MonadParam B (post val) post + _>>=_ : ∀ {A X Y Z} → {pre : X} → + {mid : A → Y} → + {post : B → Z} → + MonadParam A pre mid → + ((x : A) → MonadParam B (mid x) post) → + MonadParam B pre post \end{code} % diff --git a/src/Examples/Types.lagda.tex b/src/Examples/Types.lagda.tex index 199a356..96e5ba0 100644 --- a/src/Examples/Types.lagda.tex +++ b/src/Examples/Types.lagda.tex @@ -59,7 +59,7 @@ \end{code} % -%<*ExampleInbox> +%<*ExampleMessages> \begin{code} BoolMessage = [ ValueType Bool ]ˡ StringMessage = [ ValueType String ]ˡ @@ -69,12 +69,14 @@ RefNatMessage : MessageType RefNatMessage = ReferenceType OtherInbox ∷ [ ValueType ℕ ]ˡ - +\end{code} +% +%<*TestInbox> +\begin{code} TestInbox : InboxShape TestInbox = RefNatMessage ∷ [ BoolMessage ]ˡ \end{code} -% - +% %<*Subtyping> \begin{code} Boolbox : InboxShape