GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-23 19:42:50 -06:00
Code Issues Packages Projects Releases Wiki Activity

Transfer type checking: Added some notation explanation. Added constructor context. Added proper pattern checking operation.

Browse Source
This commit is contained in:
bringert
2006-03-03 10:56:34 +00:00
parent 0dfd55a30d
commit 54542c8423
1 changed files with 80 additions and 47 deletions
Download Patch File Download Diff File Expand all files Collapse all files

127
transfer/doc/typesystem.tex
View File

@@ -7,63 +7,96 @@
\author{Bj\"orn Bringert \\ \texttt{bringert@cs.chalmers.se}} \author{Bj\"orn Bringert \\ \texttt{bringert@cs.chalmers.se}}
\maketitle \maketitle
\section{Type Checking Algorithm}
This is the beginnings of a type checking algorithm for the This is the beginnings of a type checking algorithm for the
Transfer Core language. It is far from complete, Transfer Core language. It is far from complete,
and some of the rules make no sense at all at the moment. and some of the rules make no sense at all at the moment.
\subsection{Notation}
$\Delta$ is a set of constructor typings.
$\Gamma$ is a set of variable typings.
$\Delta;\Gamma \vdash t \uparrow A$ means that in the
variable typing context $\Gamma$ and the constructor
typing context $\Delta$, the type of $t$ can be inferred
to be $A$.
$\Delta;\Gamma \vdash t \downarrow A$ means that in the
variable typing context $\Gamma$ and the constructor
typing context $\Delta$, the type of $t$ can be
checked to be $A$.
$\Delta \vdash_p p \downarrow A; \Gamma$ means that
in the constructor typing context $\Delta$,
the pattern $p$ can matched against a value of type
$A$, and if the match succeeds, it will create
variable bindings with the typings $\Gamma$.
\subsection{Rules}
\begin{figure} \begin{figure}
\begin{mathpar} \begin{mathpar}
\inferrule[Type annotation] \inferrule[Type annotation]
{ \Gamma \vdash t \downarrow A } { \Delta;\Gamma \vdash t \downarrow A }
{ \Gamma \vdash t : A \uparrow A } { \Delta;\Gamma \vdash t : A \uparrow A }
\and \and
\inferrule[Variable] \inferrule[Variable]
{ x : A \in \Gamma } { x : A \in \Gamma }
{ \Gamma \vdash x \uparrow A } { \Delta;\Gamma \vdash x \uparrow A }
\and
\inferrule[Constructor]
{ C : A \in \Delta }
{ \Delta;\Gamma \vdash C \uparrow A }
\and \and
\inferrule[Function type] \inferrule[Function type]
{ \Gamma \vdash A \uparrow Type \\ { \Delta;\Gamma \vdash A \uparrow Type \\
\Gamma, x : A \vdash B \uparrow Type } \Delta;\Gamma, x : A \vdash B \uparrow Type }
{ \Gamma \vdash (x : A) \rightarrow B \uparrow Type } { \Delta;\Gamma \vdash (x : A) \rightarrow B \uparrow Type }
\and \and
\inferrule[Abstraction] \inferrule[Abstraction]
{ \Gamma, x : A \vdash s \uparrow B } { \Delta;\Gamma, x : A \vdash s \uparrow B }
{ \Gamma \vdash \lambda x. s \downarrow (x : A) \rightarrow B } { \Delta;\Gamma \vdash \lambda x. s \downarrow (x : A) \rightarrow B }
\and \and
\inferrule[Application] \inferrule[Application]
{ \Gamma \vdash s \uparrow (x : A) \rightarrow B \\ { \Delta;\Gamma \vdash s \uparrow (x : A) \rightarrow B \\
\Gamma \vdash t \downarrow A } \Delta;\Gamma \vdash t \downarrow A }
{ \Gamma \vdash s t \uparrow B [x / t] } { \Delta;\Gamma \vdash s t \uparrow B [x / t] }
\and \and
\inferrule[Local definition] \inferrule[Local definition]
{ \Gamma \vdash s \uparrow A \\ { \Delta;\Gamma \vdash s \uparrow A \\
\Gamma, s : A \vdash t \uparrow B } \Delta;\Gamma, s : A \vdash t \uparrow B }
{ \Gamma \vdash \textrm{let} \ x = s \ \textrm{in} \ t \uparrow B } { \Delta;\Gamma \vdash \textrm{let} \ x = s \ \textrm{in} \ t \uparrow B }
\and \and
\inferrule[Case analysis] \inferrule[Case analysis]
{ \Gamma \vdash t \uparrow A \\ { \Delta;\Gamma \vdash t \uparrow A \\
\Gamma \vdash p_1 \downarrow A, \Gamma' \\ \Delta \vdash_p p_1 \downarrow A; \Gamma' \\
\Gamma, \Gamma' \vdash g_1 \downarrow Bool \\ \Delta;\Gamma,\Gamma' \vdash g_1 \downarrow Bool \\
\Gamma, \Gamma' \vdash t_1 \uparrow B \\ \Delta;\Gamma,\Gamma' \vdash t_1 \uparrow B \\
\ldots \\ \ldots \\
p_n \textrm{match} A, \Gamma' \\ \Delta p_n \vdash_p A; \Gamma' \\
\Gamma, \Gamma' \vdash g_n \downarrow Bool \\ \Delta;\Gamma, \Gamma' \vdash g_n \downarrow Bool \\
\Gamma, \Gamma' \vdash t_n \uparrow B \\ \Delta;\Gamma, \Gamma' \vdash t_n \uparrow B \\
} }
{ \Gamma \vdash \textrm{case} \ s \ \textrm{of} \ \{ { \Delta;\Gamma \vdash \textrm{case} \ s \ \textrm{of} \ \{
p_1 \mid g_1 \rightarrow t_1; p_1 \mid g_1 \rightarrow t_1;
\ldots; \ldots;
p_n \mid g_n \rightarrow t_n p_n \mid g_n \rightarrow t_n
@@ -81,45 +114,45 @@ and some of the rules make no sense at all at the moment.
\inferrule[Variable pattern] \inferrule[Variable pattern]
{ } { }
{ x \ \textrm{match} \ A, \{ x : A \} } { \Delta \vdash_p x \downarrow \ A; \{ x : A \} }
\and \and
\inferrule[Wildcard pattern] \inferrule[Wildcard pattern]
{ } { }
{ \_ \ \textrm{match} \ A, \{ \} } { \Delta \vdash_p \_ \ \downarrow \ A; \{ \} }
\and \and
\inferrule[Constructor pattern] \inferrule[Constructor pattern]
{ C : (x_1 : T_1) \rightarrow \ldots \rightarrow T \in \Delta \\ { C : (x_1 : T_1) \rightarrow \ldots \rightarrow T \in \Delta \\
p_1 \textrm{match} T_1, \Gamma_1 \\ \Delta \vdash_p p_1 \downarrow T_1; \Gamma_1 \\
\ldots \\ \ldots \\
p_n \textrm{match} T_n, \Gamma_n \\ \Delta \vdash_p p_n \downarrow T_n; \Gamma_n \\
} }
{ C p_1 \ldots p_n \ \textrm{match} \ T, \Gamma_1, \ldots, \Gamma_n } { \Delta \vdash_p C p_1 \ldots p_n \ \downarrow \ T; \Gamma_1, \ldots, \Gamma_n }
\and \and
\inferrule[Record pattern] \inferrule[Record pattern]
{ p_1 \ \textrm{match} \ T_1, \Gamma_1 \\ { \Delta \vdash_p p_1 \ \downarrow \ T_1; \Gamma_1 \\
\ldots \\ \ldots \\
p_n \ \textrm{match} \ T_n, \Gamma_n \\ \Delta \vdash_p p_n \ \downarrow \ T_n; \Gamma_n \\
} }
{ \textrm{rec} \ \{ l_1 = p_1; \ldots; l_n = p_n \} \ \textrm{match} \ { \Delta \vdash_p \textrm{rec} \ \{ l_1 = p_1; \ldots; l_n = p_n \} \ \downarrow \
\textrm{sig} \ \{ l_1 : T_1; \ldots; l_n : T_n \}, \Gamma_1, \ldots, \Gamma_n } \textrm{sig} \ \{ l_1 : T_1; \ldots; l_n : T_n \}; \Gamma_1, \ldots, \Gamma_n }
\and \and
\inferrule[Integer literal pattern] \inferrule[Integer literal pattern]
{ } { }
{ integer \ \textrm{match} \ Integer, \{ \} } { \Delta \vdash_p integer \ \downarrow \ Integer; \{ \} }
\and \and
\inferrule[String literal pattern] \inferrule[String literal pattern]
{ } { }
{ string \ \textrm{match} \ String, \{ \} } { \Delta \vdash_p string \ \downarrow \ String; \{ \} }
\and \and
@@ -133,25 +166,25 @@ and some of the rules make no sense at all at the moment.
\begin{mathpar} \begin{mathpar}
\inferrule[Record type] \inferrule[Record type]
{ \Gamma \vdash T_1 \uparrow Type \\ { \Delta;\Gamma \vdash T_1 \uparrow Type \\
\ldots \\ \ldots \\
\Gamma, l_1 : T_1, \ldots, l_{n-1} : T_{n-1} \vdash T_n \uparrow Type } \Delta;\Gamma, l_1 : T_1, \ldots, l_{n-1} : T_{n-1} \vdash T_n \uparrow Type }
{ \Gamma \vdash \textrm{sig} \{ l_1 : T_1, \ldots, l_n : T_n \} \uparrow Type } { \Delta;\Gamma \vdash \textrm{sig} \{ l_1 : T_1, \ldots, l_n : T_n \} \uparrow Type }
\and \and
\inferrule[Record] \inferrule[Record]
{ \Gamma \vdash t_1 \uparrow T_1 \\ { \Delta;\Gamma \vdash t_1 \uparrow T_1 \\
\ldots \\ \ldots \\
\Gamma \vdash t_n \uparrow T_n [l_{n-1} / t_{n-1}] \ldots [l_1 / t_1] } \Delta;\Gamma \vdash t_n \uparrow T_n [l_{n-1} / t_{n-1}] \ldots [l_1 / t_1] }
{ \Gamma \vdash \textrm{rec} \{ l_1 = t_1, \ldots, l_n = t_n \} { \Delta;\Gamma \vdash \textrm{rec} \{ l_1 = t_1, \ldots, l_n = t_n \}
\uparrow \textrm{sig} \{ l_1 : T_1, \ldots, l_n : T_n \} } \uparrow \textrm{sig} \{ l_1 : T_1, \ldots, l_n : T_n \} }
\and \and
\inferrule[Record projection] \inferrule[Record projection]
{ \Gamma \vdash t \uparrow \textrm{sig} \{ l : T \} } { \Delta;\Gamma \vdash t \uparrow \textrm{sig} \{ l : T \} }
{ \Gamma \vdash t . l \uparrow T } { \Delta;\Gamma \vdash t . l \uparrow T }
\end{mathpar} \end{mathpar}
\caption{Records.} \caption{Records.}
@@ -164,37 +197,37 @@ and some of the rules make no sense at all at the moment.
\inferrule[Integer type] \inferrule[Integer type]
{ } { }
{ \Gamma \vdash Integer \uparrow Type } { \Delta;\Gamma \vdash Integer \uparrow Type }
\and \and
\inferrule[Integer literal] \inferrule[Integer literal]
{ } { }
{ \Gamma \vdash integer \uparrow Integer } { \Delta;\Gamma \vdash integer \uparrow Integer }
\and \and
\inferrule[Double type] \inferrule[Double type]
{ } { }
{ \Gamma \vdash Double \uparrow Type } { \Delta;\Gamma \vdash Double \uparrow Type }
\and \and
\inferrule[Double literal] \inferrule[Double literal]
{ } { }
{ \Gamma \vdash double \uparrow Double } { \Delta;\Gamma \vdash double \uparrow Double }
\and \and
\inferrule[String type] \inferrule[String type]
{ } { }
{ \Gamma \vdash String \uparrow Type } { \Delta;\Gamma \vdash String \uparrow Type }
\and \and
\inferrule[String literal] \inferrule[String literal]
{ } { }
{ \Gamma \vdash string \uparrow String } { \Delta;\Gamma \vdash string \uparrow String }
\end{mathpar} \end{mathpar}
\caption{Primitive types.} \caption{Primitive types.}