Evgenii Akentev
·
2019-01-18
Typesystem.lagda
1\chapter{Type system}\label{sec:typesys}
2
3\if{False}
4\begin{code}
5-- Imports
6open import Prelude
7
8open import Syntax
9\end{code}
10\fi
11
12Jolie type system consists of trees because they are matched to variables, which are trees. Variables are simplified by enumeration, as it was mentioned before, and so types too.
13
14Therefore, basic types of Jolie are just usual types, which are commonly-used native types such as \jkeyw{int}, \jkeyw{double}, \jkeyw{long}, \jkeyw{boolean} and \jkeyw{string}. Also, Jolie has the following types:
15
16\begin{itemize}
17\item \jkeyw{raw}, representing raw data streams as byte arrays.
18\item \jkeyw{void}, indicating no value.
19\item \jkeyw{any}, as a placeholder for any native types.
20\end{itemize}
21
22In order to be able to do type checking of a Jolie program, I provide the implementation of types and typing rules in Agda.
23
24\section{Types declaration}
25
26The main Jolie native types (excluding any) are expressed in the following way:
27
28\begin{code}
29data Type : Set where
30 bool int double long string raw void : Type
31\end{code}
32
33Usually, the context of a program is a list of variables, but to service all three layers (comprising communication of services) there is a special type called \AgdaDatatype{TypeDecl}. It has five constructors: the first two (unidirectional and bidirectional) are for output communication. The left part of such bindings consists of an operation name and a location of a hosting service. The next two are for input communication and the last one is for variables.
34
35\begin{code}
36data TypeDecl : Set where
37 -- o@l : <T>
38 _at_∶<_> : Operation → Location → Type → TypeDecl
39
40 -- o@l : <T, T>
41 _at_∶<_,_> : Operation → Location → Type → Type → TypeDecl
42
43 -- o : <T>
44 _∶<_> : Operation → Type → TypeDecl
45
46 -- o : <T, T>
47 _∶<_,_> : Operation → Type → Type → TypeDecl
48
49 -- x : T
50 _∶_ : Variable → Type → TypeDecl
51\end{code}
52
53Therefore, the type of context is a vector of \AgdaDatatype{TypeDecl}.
54
55\begin{code}
56Ctx : ℕ → Set
57Ctx = Vec TypeDecl
58\end{code}
59
60Although the type of context is defined, it's not enough, because programs in Jolie can be parallel. In ~\cite{nielsen2013type}, there is a constructor of a disjoint union of the \AgdaDatatype{TypeDecl} to make programs parallel. In this project, the disjoint union is defined as a wrapper of \AgdaDatatype{TypeDecl}. I define one more type called \AgdaDatatype{Context} to cover such situations. It has only two constructors: the first one just takes \AgdaDatatype{Ctx\ n} and the second one consists of two elements of itself.
61
62\begin{code}
63data Context : Set where
64 ⋆ : ∀ {n} → Ctx n → Context
65 & : Context → Context → Context
66\end{code}
67
68The type of context is not a vector anymore, so here is the definition of such type that will express the fact of the presence of \AgdaDatatype{TypeDecl} in \AgdaDatatype{Context}:
69
70\begin{code}
71infix 4 _∈_
72data _∈_ : TypeDecl → Context → Set where
73\end{code}
74
75I define the type \AgdaDatatype{\_\in\_} to be infix with priority $4$. This type takes other two types: \AgdaDatatype{TypeDecl} and \AgdaDatatype{Context}. It means that by constructing the type $ T \in C $, where $ T $ has type \AgdaDatatype{TypeDecl} and $ C $ has type \AgdaDatatype{Context}, the proposition "T is an element of C" is being formulated.
76
77Let's start with the first constructor of \AgdaDatatype{Context}: \AgdaInductiveConstructor{⋆}. It is the simple case when the context is just a \AgdaDatatype{Ctx} $n$. The constructor \AgdaInductiveConstructor{here-⋆} means that some element $x$ is the first element of context. In the second case, \AgdaInductiveConstructor{there-⋆} takes the term of type $x ∈ ⋆ xs$, which states that $x$ is an element of $xs$ with type \AgdaDatatype{Ctx} $n$, and states that we can add any element to $xs$.
78\begin{code}
79 here-⋆ : ∀ {n} {x} {xs : Ctx n}
80 → x ∈ ⋆ (x ∷ xs)
81
82 there-⋆ : ∀ {n} {x y} {xs : Ctx n}
83 (x∈xs : x ∈ ⋆ xs)
84 → x ∈ ⋆ (y ∷ xs)
85\end{code}
86
87The constructors \AgdaInductiveConstructor{here-left-\&} and \AgdaInductiveConstructor{here-right-\&} are for the second case when the context is a disjoint union. They state that $x$ is an element of the left context or the right context of the disjoint union.
88
89\begin{code}
90 here-left-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m}
91 → x ∈ & (⋆ (x ∷ xs)) (⋆ ys)
92
93 here-right-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m}
94 → x ∈ & (⋆ xs) (⋆ (x ∷ ys))
95\end{code}
96
97The two last constructors are similar to \AgdaInductiveConstructor{there-⋆}, but for the disjoint union.
98
99\begin{code}
100 there-left-& : ∀ {n m} {x y} {xs : Ctx n} {ys : Ctx m}
101 (x∈xs : x ∈ & (⋆ xs) (⋆ ys))
102 → x ∈ & (⋆ (y ∷ xs)) (⋆ ys)
103
104 there-right-& : ∀ {n m} {x y} {xs : Ctx n} {ys : Ctx m}
105 (x∈xs : x ∈ & (⋆ xs) (⋆ ys))
106 → x ∈ & (⋆ xs) (⋆ (y ∷ ys))
107\end{code}
108
109To demonstrate the examples of using the type of context and the type of presence described before I need to define preliminary types. Let $y$ and $z$ are variables:
110
111\begin{code}
112y z : Variable
113y = 0
114z = 1
115\end{code}
116
117The type of variables doesn't matter in this case, so it's just a boolean.
118
119\begin{code}
120Ty : Type
121Ty = bool
122\end{code}
123
124$C1$, $C2$, $C3$ and $C4$ are contexts. $C1$ is a simple context with only one element \AgdaDatatype{y} $:$ \AgdaDatatype{Ty} (variable \AgdaDatatype{y} with type \AgdaDatatype{Ty}), while $C2$ is a simple context too, but with two variables \AgdaDatatype{z} and \AgdaDatatype{y}. $C3$ and $C4$ are disjoint union context for parallel behaviours. $C3$ has $C1$ as a left context and its right context is empty. $C4$ has $C2$ as a right context and its left context is empty.
125
126\begin{code}
127C1 C2 C3 C4 : Context
128C1 = ⋆ (y ∶ Ty ∷ [])
129C2 = ⋆ (z ∶ Ty ∷ y ∶ Ty ∷ [])
130C3 = & C1 (⋆ [])
131C4 = & (⋆ []) C2
132\end{code}
133
134Here are examples which use the type of context and the type of presence items in context:
135
136\begin{itemize}
137
138\item The first example is pretty simple. I state that the variable \AgdaDatatype{y} of type \AgdaDatatype{Ty} is an element of the context $C1$. The proof of such statement, which is a type at the same time, is just a term \AgdaInductiveConstructor{here-⋆} because $C1$ has only one element and \AgdaInductiveConstructor{here-⋆} states that \AgdaDatatype{y} $:$ \AgdaDatatype{Ty} is the first element of $C1$.
139
140\begin{code}
141y∈C1 : (y ∶ Ty) ∈ C1
142y∈C1 = here-⋆
143\end{code}
144
145\item In $C2$ the variable \AgdaDatatype{y} is the second element. To express that fact I need to use \AgdaInductiveConstructor{there-⋆}, because \AgdaDatatype{\_\in\_} is an inductive type. \AgdaInductiveConstructor{there-⋆} takes the term of type $x$ \AgdaDatatype{\in} \AgdaInductiveConstructor{⋆} $xs$, which is \AgdaInductiveConstructor{here-⋆} in this case, and states that $x$ is somewhere in this context.
146
147\begin{code}
148y∈C2 : (y ∶ Ty) ∈ C2
149y∈C2 = there-⋆ here-⋆
150\end{code}
151
152\item In this case, \AgdaDatatype{y} is the first element of the left context of the disjoint union context $C3$, that's why \AgdaInductiveConstructor{here-left-\&} is used.
153
154\begin{code}
155y∈C3 : (y ∶ Ty) ∈ C3
156y∈C3 = here-left-&
157\end{code}
158
159\item The last example is similar to examples with $C2$ and $C3$. $C4$ is a disjoint union context where the \AgdaDatatype{y} variable is in the right context on the second place.
160
161\begin{code}
162y∈C4 : (y ∶ Ty) ∈ C4
163y∈C4 = there-right-& here-right-&
164\end{code}
165
166\end{itemize}
167
168Next, I define the type of a correctly typed expression with variables from context $ \Gamma $.
169
170\begin{code}
171data _⊢ₑ_∶_ (Γ : Context) : Expr → Type → Set where
172 expr-t : {s : Expr} {b : Type}
173 → Γ ⊢ₑ s ∶ b
174\end{code}
175
176The \AgdaInductiveConstructor{expr-t} constructor is a simplified version because it should check all variables in the expression $s$ from context $ \Gamma $. In this work, it's assumed that all given expressions are correct.
177
178\input{Typingrules}