repos / bachelor-thesis.git

Typingrules.lagda

  1\section{Typing rules for behaviour layer}
  2
  3\if{False}
  4\begin{code}
  5-- Imports
  6open import Prelude
  7open import Syntax
  8open import Typesystem
  9\end{code}
 10\fi
 11
 12There were created 28 typing rules for behaviour layer during the development. Some of them are almost similar to the rules from the basement of this work~\cite{nielsen2013type}. I demonstrate the subset of the typing rules.
 13
 14In ~\cite{nielsen2013type}, if a behaviour $b$ is typed with respect to an environment $\Gamma$ and changes it during type checking to an environment $\Gamma_1$, then it is written as $\Gamma \vdash_{B} b \vartriangleright \Gamma_1$ in the form of Hoare triple.
 15
 16\begin{code}
 17data _⊢B_▹_ : Context → Behaviour → Context → Set where
 18\end{code}
 19
 20The following constructors of this type express the typing rules and they are used for type checking behaviours. The first constructor is for the \AgdaInductiveConstructor{nil} behaviour. Since \AgdaInductiveConstructor{nil} does nothing, the context before and the context after are equal.
 21
 22\begin{code}
 23  t-nil : {Γ : Context}
 24        → Γ ⊢B nil ▹ Γ
 25\end{code}
 26
 27The \AgdaInductiveConstructor{t-if} constructor is intended for \AgdaInductiveConstructor{if\_then\_else} behaviour. It takes three arguments: a type which states that the expression $e$ has type \AgdaInductiveConstructor{bool}, two types which state that the behaviours $b_1$ and $b_2$ are well-typed. The result of this constructor is well typed \AgdaInductiveConstructor{if\_then\_else} behaviour.
 28
 29\begin{code}
 30  t-if : {Γ Γ₁ : Context} {b₁ b₂ : Behaviour} {e : Expr}
 31       → Γ ⊢ₑ e ∶ bool
 32       → Γ ⊢B b₁ ▹ Γ₁
 33       → Γ ⊢B b₂ ▹ Γ₁
 34       → Γ ⊢B if e then b₁ else b₂ ▹ Γ₁
 35\end{code}
 36
 37To construct a well-typed \AgdaInductiveConstructor{while[\_]\_} behaviour there is the \AgdaInductiveConstructor{t-while} constructor which takes a well-typed with respect to the environment expression $e$ and a well-typed behaviour $b$. The typing rule does not change the environment after the behaviour.
 38
 39\begin{code}
 40  t-while : {Γ : Context} {b : Behaviour} {e : Expr}
 41          → Γ ⊢ₑ e ∶ bool
 42          → Γ ⊢B b ▹ Γ
 43          → Γ ⊢B while[ e ] b ▹ Γ
 44\end{code}
 45
 46The following constructor is for sequential programs. It takes two well typed behaviours and returns a well-typed \AgdaInductiveConstructor{seq} behaviour. Notice how contexts of typing rules are arranged. $\Gamma \vdash_{B} b_1 \vartriangleright \Gamma_1$ and $\Gamma_1 \vdash_{B} b_2 \vartriangleright \Gamma_2$ are connected into $\Gamma \vdash_{B} b_1 : b_2 \vartriangleright \Gamma_2$.
 47
 48\begin{code}
 49  t-seq : {Γ Γ₁ Γ₂ : Context} {b₁ b₂ : Behaviour}
 50        → Γ ⊢B b₁ ▹ Γ₁
 51        → Γ₁ ⊢B b₂ ▹ Γ₂
 52        → Γ ⊢B b₁ ∶ b₂ ▹ Γ₂
 53\end{code}
 54
 55The \AgdaInductiveConstructor{t-par} constructor is for \AgdaInductiveConstructor{\_∥\_} (`parallel`) behaviour. The parallel behaviour is typable if each its thread is well typed and the resulting environments are disjoint. In this work, I assume that the last statement is true.
 56
 57\begin{code}
 58  t-par : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b₁ b₂ : Behaviour}
 59        → Γ₁ ⊢B b₁ ▹ Γ₁'
 60        → Γ₂ ⊢B b₂ ▹ Γ₂'
 61        → (& Γ₁ Γ₂) ⊢B b₁ ∥ b₂ ▹ (& Γ₁' Γ₂')
 62\end{code}
 63
 64The next four constructors are for assignment behaviour. I start with the \AgdaInductiveConstructor{t-assign-new} typing rule which is intended for a simple context. It takes a fact that an expression $e$ is well-typed with respect to an environment $\Gamma$, a fact that a variable $x$ is not in $\Gamma$ and returns an assignment behaviour where the resulting environment has variable $x$ with the type of expression $e$.
 65
 66\begin{code}
 67  t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
 68               → ⋆ Γ ⊢ₑ e ∶ Tₑ
 69               → ¬ (x ∶ Tₓ ∈ ⋆ Γ)
 70               → ⋆ Γ ⊢B x ≃ e ▹ ⋆ (x ∶ Tₑ ∷ Γ)
 71\end{code}
 72
 73This constructor is for the case when the initial context is a disjoint union and the assignment of variable $x$ is done in the left context.
 74
 75\begin{code}
 76  t-assign-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m}  {x : Variable}
 77                      {e : Expr} {Tₓ Tₑ : Type}
 78                    → & (⋆ Γ) (⋆ Γ₁) ⊢ₑ e ∶ Tₑ
 79                    → ¬ (x ∶ Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
 80                    → & (⋆ Γ) (⋆ Γ₁) ⊢B x ≃ e ▹ & (⋆ (x ∶ Tₑ ∷ Γ)) (⋆ Γ₁)
 81\end{code}
 82
 83The constructor \AgdaInductiveConstructor{t-assign-new-right} is similar to the previous one. It adds variable $x$ in the right context of a disjoint union.
 84
 85\begin{code}
 86  t-assign-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m}  {x : Variable}
 87                       {e : Expr} {Tₓ Tₑ : Type}
 88                     → & (⋆ Γ) (⋆ Γ₁) ⊢ₑ e ∶ Tₑ
 89                     → ¬ (x ∶ Tₓ ∈ & (⋆ Γ) (⋆ Γ₁))
 90                     → & (⋆ Γ) (⋆ Γ₁) ⊢B x ≃ e ▹ & (⋆ Γ) (⋆ (x ∶ Tₑ ∷ Γ₁))
 91\end{code}
 92
 93The next constructor is for an assignment behaviour when the variable is already defined in the initial context. It requires a type of expression to be equal to a type of variable.
 94
 95\begin{code}
 96  t-assign-exists : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
 97                  → Γ ⊢ₑ e ∶ Tₑ
 98                  → x ∶ Tₓ ∈ Γ
 99                  → Tₑ ≡ Tₓ
100                  → Γ ⊢B x ≃ e ▹ Γ
101\end{code}