From d7ed5ab556eb6d2a7921ea38aa91a5b8e2e236f1 Mon Sep 17 00:00:00 2001 From: Pierre Krafft Date: Thu, 31 May 2018 18:50:45 +0200 Subject: [PATCH] Writing --- src/ActorMonad.lagda.tex | 39 ++++++++++++------- src/Examples/MonadParameterized.lagda.tex | 10 +++++ src/Examples/SizedStream.lagda.tex | 6 +++ src/Selective/SimulationEnvironment.lagda.tex | 12 ++++-- 4 files changed, 49 insertions(+), 18 deletions(-) diff --git a/src/ActorMonad.lagda.tex b/src/ActorMonad.lagda.tex index 07ba6c5..468f626 100644 --- a/src/ActorMonad.lagda.tex +++ b/src/ActorMonad.lagda.tex @@ -38,7 +38,7 @@ The \AgdaFunction{InboxShape} is a variant type that details all the messages that can be received from an inbox. Every message sent to an actor will have exactly one of the types that is listed, -which we communicate as a tag attached to the message (see section \ref{sec:messages}). +which we communicate as a tag attached to the message (see section~\ref{sec:messages}). We can think of the \AgdaFunction{InboxShape} as a set of types, and every message coming paired with a proof that the message is a type from that set. To know what type a message has you have to inspect the proof, @@ -183,18 +183,10 @@ 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. -Following are some examples comparing a λ-calculus with names -and a λ-calculus using de Bruijn indices. - -\begin{table}[htbp] -\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) $ \\ -\end{tabular} -\end{table} +Figure~\ref{fig:debruijn} shows some examples comparing a λ-calculus with names +to a λ-calculus using de Bruijn indices. + +\input{include/figures/debruijn} 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 as @@ -202,6 +194,7 @@ We choose to represent the indices as the membership proposition in order to make the de Bruijn indices correct by construction. This lets us define the type judgement $Γ ⊢ T$ as: + \begin{minipage}{\textwidth} \begin{code} ReferenceTypes = List InboxShape @@ -241,7 +234,7 @@ since different actors receiving the reply will have a different \AgdaFunction{InboxShape}. This pattern, together with a selective receive construct, can be used to implement synchronous calls, -which we explore in chapter \ref{chap:selective_receive}. +which we explore in chapter~\ref{chap:selective_receive}. % %<*Messages> @@ -269,7 +262,11 @@ send-field-content : TypingContext → MessageField → Set₁ send-field-content Γ (ValueType A) = Lift A send-field-content Γ (ReferenceType requested) = Γ ⊢>: requested +\end{code} +\end{minipage} +\begin{minipage}{\textwidth} +\begin{code} record SendMessage (To : InboxShape) (Γ : TypingContext) : Set₁ where constructor SendM @@ -287,7 +284,7 @@ Instead we find the unit type \AgdaDatatype{⊤}, which has no computational content at all. The answer to this puzzle lies in that receiving a message will have the side-effect of adding the references from every reference field to the variable context. -We saw in figure \ref{fig:actorm} that the shape of the variable typing context is maintained +We saw in figure~\ref{fig:actorm} that the shape of the variable typing context is maintained in the type of the monad, making it easy to create indices into the variable context without making them a part of the message. @@ -299,19 +296,31 @@ receive-field-content : MessageField → Set receive-field-content (ValueType A) = A receive-field-content (ReferenceType Fw) = ⊤ +\end{code} +\end{minipage} +\begin{minipage}{\textwidth} +\begin{code} record Message (To : InboxShape) : Set₁ where constructor Msg field {MT} : MessageType received-message-type : MT ∈ To received-fields : All receive-field-content MT +\end{code} +\end{minipage} +\begin{minipage}{\textwidth} +\begin{code} extract-references : MessageType → ReferenceTypes extract-references [] = [] extract-references (ValueType x ∷ mt) = extract-references mt extract-references (ReferenceType T ∷ mt) = T ∷ extract-references mt +\end{code} +\end{minipage} +\begin{minipage}{\textwidth} +\begin{code} add-references : ∀ {To} → TypingContext → Message To → TypingContext add-references Γ (Msg {MT} x x₁) = extract-references MT ++ Γ \end{code} diff --git a/src/Examples/MonadParameterized.lagda.tex b/src/Examples/MonadParameterized.lagda.tex index d3ec816..a5dd4e1 100644 --- a/src/Examples/MonadParameterized.lagda.tex +++ b/src/Examples/MonadParameterized.lagda.tex @@ -33,12 +33,17 @@ % %<*MonadFile> +\begin{minipage}{\textwidth} \begin{code} data FileState : Set where Open : String → FileState Closed : FileState +\end{code} +\end{minipage} +\begin{minipage}{\textwidth} +\begin{code} data FileMonad : (A : Set) → FileState → (A → FileState) → Set₁ where return : ∀ {A post} → (val : A) → FileMonad A (post val) post _>>=_ : ∀ {A B pre mid post} → @@ -48,12 +53,17 @@ OpenFile : String → FileMonad FileState Closed (λ x → x) CloseFile : ∀ { s } → FileMonad ⊤ (Open s) (λ _ → Closed) WriteFile : ∀ { s } → String → FileMonad ⊤ (Open s) (λ _ → Open s) +\end{code} +\end{minipage} +\begin{minipage}{\textwidth} +\begin{code} writeHello : FileMonad ⊤ Closed (λ _ → Closed) writeHello = OpenFile "world.txt" >>= λ { Closed → return _ ; (Open _) → WriteFile "hello" >>= λ _ → CloseFile } \end{code} +\end{minipage} % diff --git a/src/Examples/SizedStream.lagda.tex b/src/Examples/SizedStream.lagda.tex index e956b47..f7b0345 100644 --- a/src/Examples/SizedStream.lagda.tex +++ b/src/Examples/SizedStream.lagda.tex @@ -22,15 +22,21 @@ \end{code} % %<*Fib> +\begin{minipage}{\textwidth} \begin{code} zipWith : (i : Size) {A B C : Set} → (A → B → C) → Stream i A → Stream i B → Stream i C (zipWith i f xs ys) .head = f (xs .head) (ys .head) (zipWith i f xs ys) .tail j = zipWith j f (xs .tail j) (ys .tail j) +\end{code} +\end{minipage} +\begin{minipage}{\textwidth} +\begin{code} fib : (i : Size) → Stream i ℕ fib i .head = 0 fib i .tail j .head = 1 fib i .tail j .tail k = zipWith k _+_ (fib k) (fib j .tail k) \end{code} +\end{minipage} % diff --git a/src/Selective/SimulationEnvironment.lagda.tex b/src/Selective/SimulationEnvironment.lagda.tex index 03286bf..35b9f65 100644 --- a/src/Selective/SimulationEnvironment.lagda.tex +++ b/src/Selective/SimulationEnvironment.lagda.tex @@ -453,14 +453,20 @@ is-ls : (heads) ++ (el ∷ tails) ≡ ls \end{code} % -%<*FoundInList> +%<*matches-filter> \begin{code} matches-filter : ∀{a} {A : Set a} → (f : A → Bool) → A → Set matches-filter f v = f v ≡ true - +\end{code} +% +%<*misses-filter> +\begin{code} misses-filter : ∀{a} {A : Set a} → (f : A → Bool) → A → Set misses-filter f v = f v ≡ false - +\end{code} +% +%<*FoundInList> +\begin{code} data FoundInList {a : Level} {A : Set a} (ls : List A) (f : A → Bool) :