impl-paper/typechecking.tex · Idris-dev

git.iko.soy/Idris-dev

on 8bf44c2 help sign in

Idris-dev/impl-paper/typechecking.tex

265 lines 8.5 kB history raw

1\section{The Core Type Theory}

3High level \Idris{} programs, as described in Section \ref{sect:hll} are

4\remph{elaborated} to a small core language, \TT{}, then type checked.

5\TT{} is a dependently typed $\lambda$-calculus with inductive families

6and pattern matching definitions similar to UTT~\cite{luo1994}, and building

7on an earlier implementation, \Ivor{}~\cite{Brady2006b}.

8We keep the

9core language as small as is reasonable, which has several advantages: it is

10easy to type check, since type checking dependent type theory is well understood

11~\cite{loh2010tutorial}; and it is easy to transform, optimise and compile. Keeping

12the core language small increases our confidence that these important components of

13the language are correct. In this section, we describe \TT{} and

14its semantics.

16\subsection{\TT{} syntax}

18The syntax of \TT{} expressions is given in Figure \ref{ttsyn}. This defines:

20\begin{itemize}

21\item \demph{Terms}, $\vt$, which are variables, bindings, applications or constants.

22\item \demph{Bindings}, $\vb$, which are lambda abstractions, let bindings, or function spaces.

23\item \demph{Constants}, $\vc$, which are integer or string literals, or $\Type_i$, the

24type of types.

25\end{itemize}

27We may also write the function space $\all{\vx}{\vS}\SC\vT$ as $(\vx\Hab\vS)\to\vT$,

28or $\vS\to\vT$ if $\vx$ is not free in $\vT$, to make the notation more consistent with

29the high level language. Universe levels on sets ($\Type_i$) may be left implicit and

30inferred by the machine~\cite{pollack1990implicit}.

32\FFIG{

33\begin{array}{rll@{\hg}rll}

34\vt ::= & \vc & (\mbox{constants}) &

35\hg\vb ::= & \lam{\vx}{\vt} & (\mbox{abstraction}) \\

37 \mid & \vx & (\mbox{variable}) &

38 \mid & \LET\:\vx\defq\vt\Hab\vt & (\mbox{let binding}) \\

40 \mid & \vb\SC\:\vt & (\mbox{binding}) &

41 \mid & \all{\vx}{\vt} & (\mbox{function space}) \\

43 \mid & \vt\:\vt & (\mbox{application}) &

44% \mid & \pat{\vx}{\vt} & (\mbox{pattern variable}) \\

45% & & &

46% \mid & \pty{\vx}{\vt} & (\mbox{pattern type}) \\

47\medskip\\

48 \vc ::= & \Type_i & (\mbox{type universes}) \\

49 \mid & \vi & (\mbox{integer literal}) \\

50 \mid & \VV{str} & (\mbox{string literal}) \\

51\end{array}

52}

53{\TT{} expression syntax}

54{ttsyn}

56\subsection{\TT{} semantics}

58The static and dynamic semantics of \TT{} are defined mutually, since

59evaluation relies on a well-typed term, and type checking relies on

60evaluation. Everything is defined relative

61to a context, $\Gamma$. The empty context

62is valid, as is a context extended with a $\lambda$, $\forall$ or

63$\LET$ binding:

65\DM{

66\Axiom{\proves\RW{valid}}

67\hg

68\Rule{\Gamma\proves\RW{valid}}

69{\Gamma;\vb\proves\RW{valid}}

70}

72\subsubsection{Evaluation}

74Conceptually, evaluation of \TT{} is defined by contraction schemes, given in Figure

75\ref{ttcontract}. \demph{Contraction}, relative to a context $\Gamma$, is given

76by one of the following schemes:

78\begin{itemize}

79\item $\beta$-contraction, which substitutes a value applied to a $\lambda$-binding for

80the bound variable. We define $\beta$-constraction simply by replacing the $\lambda$-binding

81with a $\LET$ binding.

82\item $\delta$-contraction, which replaces a $\LET$ bound variable with its value.

83\end{itemize}

85\demph{Reduction} ($\reduces$) is the structural closure of contraction, and evaluation

86is ($\reducesto$) is the transitive closure of reduction. \demph{Conversion} ($\converts$)

87is the smallest equivalence relation closed under reduction. If $\Gamma\proves\vx\converts\vy$

88then $\vy$ can be obtained from $\vx$ by a finite, possibly empty, sequence of

89contractions and reversed contractions. Terms which are convertible are also said to

90be computationally equal.

92\FFIG{

93\begin{array}{lc}

94\beta\mathrm{-contraction} &

95\Axiom{

96\Gamma\proves(\lam{\vx}{\vS}\SC\vt)\:\vs\leadsto\LET\:\vx\defq\vs\Hab\vS\SC\vt

97} \\

98\delta\mathrm{-contraction} &

99\Axiom{

100\Gamma;\LET\:\vx\defq\vs\Hab\vS;\Gamma'

101\proves

102\vx\leadsto\vs

103}

104\end{array}

105}

106{\TT{} contraction schemes}

107{ttcontract}

108

109\subsubsection{Cumulativity}

110

111Figure \ref{cumul} gives the \demph{cumulativity} relation.

112

113\FFIG{

114\begin{array}{c}

115\Rule{\Gamma\proves\vS\converts\vT}

116{\Gamma\proves\vS\cumul\vT}

117\hg

118\Axiom{\Gamma\proves\Type_n\cumul\Type_{n+1}}

119\\

120\Rule{\Gamma\proves\vR\cumul\vS\hg\Gamma\proves\vS\cumul\vT}

121{\Gamma\proves\vR\cumul\vT}

122\\

123\Rule{\Gamma\proves\vS_1\converts\vS_2\hg\Gamma;\vx\Hab\vS_1\proves\vT_1\cumul\vT_2}

124{\Gamma\proves\all{\vx}{\vS_1}\SC\vT_1\cumul\all{\vx}{\vS_2}{\vT_2}}

125\end{array}

126}

127{Cumulativity}

128{cumul}

129

130\subsubsection{Typing rules}

131

132\FFIG{\begin{array}{c}

133\mathsf{Type}\:

134\Rule{\Gamma\proves\RW{valid}}

135{\Gamma\vdash\Type_n\Hab\Type_{n+1}}

136\\

137\mathsf{Var}_1\:

138\Rule{(\lam{\vx}{\vS})\in\Gamma}

139{\Gamma\vdash\vx\Hab\vS}

140\hg

141\mathsf{Var}_2\:

142\Rule{(\all{\vx}{\vS})\in\Gamma}

143{\Gamma\vdash\vx\Hab\vS}

144\hg

145\mathsf{Val}\:

146\Rule{(\LET\:\vx\Hab\vS\defq\vs)\in\Gamma}

147{\Gamma\vdash\vx\Hab\vS}

148\\

149%\mathsf{Pat}_1\:

150%\Rule{(\pat{\vx}{\vS})\in\Gamma}

151%{\Gamma\vdash\vx\Hab\vS}

152%\hg

153%\mathsf{Pat}_2\:

154%\Rule{(\pty{\vx}{\vS})\in\Gamma}

155%{\Gamma\vdash\vx\Hab\vS}

156\\

157\mathsf{App}\:

158\Rule{\Gamma\vdash\vf\Hab\fbind{\vx}{\vS}{\vT}\hg\Gamma\vdash\vs\Hab\vS}

159{\Gamma\vdash\vf\:\vs\Hab\vT[\vs/\vx]} % \LET\:\vx\Hab\vS\:\defq\:\vs\:\IN\:\vT}

160\\

161\mathsf{Lam}\:

162\Rule{\Gamma;\lam{\vx}{\vS}\vdash\ve\Hab\vT\hg\Gamma\proves\fbind{\vx}{\vS}{\vT}\Hab\Type_n}

163{\Gamma\vdash\lam{\vx}{\vS}.\ve\Hab\fbind{\vx}{\vS}{\vT}}

164\\

165\mathsf{Forall}\:

166\Rule{\Gamma;\all{\vx}{\vS}\vdash\vT\Hab\Type_m\hg\Gamma\vdash\vS\Hab\Type_n}

167{\Gamma\vdash\fbind{\vx}{\vS}{\vT}\Hab\Type_p}

168\:(\exists\vp.\vm\le\vp,\:\vn\le\vp)

169\\

170\mathsf{Let}\:

171\Rule{\begin{array}{c}\Gamma\proves\ve_1\Hab\vS\hg

172 \Gamma;\LET\:\vx\defq\ve_1\Hab\vS\proves\ve_2\Hab\vT\\

173 \Gamma\proves\vS\Hab\Type_n\hg

174 \Gamma;\LET\:\vx\defq\ve_1\Hab\vS\proves\vT\Hab\Type_n\end{array}

175 }

176{\Gamma\vdash\LET\:\vx\defq\ve_1\Hab\vS\SC\:\ve_2\Hab

177 \vT[\ve_1/\vx]}

178%\Let\:\vx\Hab\vS\defq\ve_1\:\IN\:\vT}

179\\

180

181\mathsf{Conv}\:

182\Rule{\Gamma\proves\vx\Hab\vA\hg\Gamma\proves\vA'\Hab\Type_n\hg

183 \Gamma\proves\vA\cumul\vA'}

184 {\Gamma\proves\vx\Hab\vA'}

185\end{array}

186}

187{Typing rules for \TT{}}

188{typerules}

189

190\subsection{Inductive Families}

191

192Inductive families \cite{dybjer1994inductive} are a form of simultaneously

193defined collection of algebraic data types (such as Haskell

194\texttt{data} declarations) which can be parametrised over

195\remph{values} as well as types. An inductive family is declared

196in a similar style to a Haskell GADT declaration~\cite{pj2006gadts}

197as

198follows, using the de Bruijn telescope notation, $\tx$, to indicate a

199sequence of zero or more $\vx$:

200

201\DM{

202\AR{

203\Data\hg\TC{T}\:(\tx\Hab\ttt)\Hab\vt\hg\Where\hg

204\DC{c}_1\Hab\vt\:\mid\:\ldots\:\mid\:\DC{c}_n\Hab\vt

205}

206}

207

208Constructors may take recursive arguments in the family

209$\TC{T}$. Furthermore these arguments may themselves be indexed by another type ---

210if such indices do not involve $\TC{T}$ then the constructor is

211\demph{strictly positive}, which ensures that recursive arguments of the

212constructor are structurally smaller than the value itself.

213

214For example, the \Idris{} data type \tTC{Nat} would be declared in \TT{} as follows:

215

216\DM{

217\Data\hg\Nat\Hab\Type\hg\Where\hg\Z\Hab\Nat\:\mid\:\suc\Hab\fbind{\vk}{\Nat}{\Nat}

218}

219

220A data type may have zero or more parameters (which are invariant

221across a structure) and a number of indices, given by the type. For

222example, the \TT{} equivalent of \tTC{List} is parametrised over its element type:

223

224\DM{

225\AR{

226\Data\hg\List\:(\va\Hab\Type)\Hab\Type\hg\Where

227\ARd{

228& \nil\Hab\List\:\va\\

229\mid & (\cons)\Hab\fbind{\vx}{\va}{\fbind{\vxs}{\List\:\va}{\List\:\va}}

230}

231}

232}

233

234Types can be

235parametrised over values. Using this, we can declare the type of

236vectors (lists with length), where the empty list is statically known

237to have length zero, and the non empty list is statically known to

238have a non zero length. The \TT{} equivalent of \tTC{Vect} is parametrised over its element type,

239like $\List$, but \remph{indexed} over its length. Note also that the length

240index $\vk$ is given \remph{explicitly}.

241

242\DM{

243\AR{

244\Data\hg\Vect\:(\va\Hab\Type)\Hab\Nat\to\Type\hg\Where \\

245\hg\hg\ARd{

246& \nil\Hab\Vect\:\va\:\Z\\

247\mid & (\cons)\Hab\fbind{\vk}{\Nat}{

248\fbind{\vx}{\va}{\fbind{\vxs}{\Vect\:\va\:\vk}{\Vect\:\va\:(\suc\:\vk)}}

249}

250}

251}

252}

253

254\subsection{Pattern matching definitions}

255

256\subsection{The Development Calculus \TTdev}

257

258\TTdev{} is \TT{} extended with hole binders, Oleg-style~\cite{McBride1999}.

259

260\subsection{The $\MO{Elab}$ meta-language}

261

262

263\begin{itemize}

264\item $\MO{Check}\:\vt\:\cq\:(\vt, \vt)$

265\end{itemize}