ca6c931 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Paper revisions

ca6c931Edwin Brady13 years ago

papers/impl-paper/elaboration.tex+10−4

compare with master

unifiedsplit

@@ -31,7 +31,7 @@ the type theory needs to support

31To achieve this, we extend \TT{} with \remph{holes},

32calling the extended calculus \TTdev{}.

33Holes stand for the parts of programs which have not yet been

34−instantiated; this largely follows the \Oleg{} development

34+instantiated; this largely follows the Oleg development

35calculus~\cite{McBride1999}.

37The basic idea is to extend the syntax for binders with a \remph{hole}

@@ -193,7 +193,7 @@ allows the elaborator to use pattern bindings from the left

193hand side of a pattern matching definition in the term on the right hand side.

194

195

196−\newcommand{\Check}{\MO{Check}_\Gamma}

196+\renewcommand{\Check}{\MO{Check}_\Gamma}

197\newcommand{\Eval}{\MO{Normalise}_\Gamma}

198\newcommand{\Unify}{\MO{Unify}_\Gamma}

199\newcommand{\PrimUnify}{\MO{PrimUnify}_\Gamma}

@@ -1077,7 +1077,10 @@ elaboration will fail.

1077If we are building the left hand side of a pattern clause, however, there is a

1078problem, as it is the left hand side which \remph{defines} variables. In this

1079context, we assume that attempting to elaborate a variable which does not type

1080−check means that the variable is a pattern variable:

1080+check means that the variable is a pattern variable\footnote{In Haskell,

1081+pattern variables are all lower case, so type checking can assume that a

1082+lower case name in a pattern refers to a variable. In \Idris{} however, a

1083+name in a pattern may refer to a function, if forced by some dependency.}:

1081

1084

1082\DM{

1085\DM{

1083\ttpinterp{\vx}\;\mq\;

1086\ttpinterp{\vx}\;\mq\;

@@ -1498,7 +1501,10 @@ $\vp$ with the name $\ve$.

1498\vec{\MO{Elab}}\;\tc'\\

1501\vec{\MO{Elab}}\;\tc'\\

1499\RW{return}\;(\RW{var}\;\tp\SC\VV{lhs}\;=\;\vx'\;\tp_{w}\;\vw'\;\tp_{n})

1502\RW{return}\;(\RW{var}\;\tp\SC\VV{lhs}\;=\;\vx'\;\tp_{w}\;\vw'\;\tp_{n})

1500}

1503}

1501−\medskip\\

1504+}

1505+}

1506+\DM{

1507+\AR{

1502\MO{MatchWith}\;\tp_w\;\tp_n\;\ttt\;(\vx\;\tw\;\mid\;\ve\;\VV{rhs})\;\mq\\

1508\MO{MatchWith}\;\tp_w\;\tp_n\;\ttt\;(\vx\;\tw\;\mid\;\ve\;\VV{rhs})\;\mq\\

1503\hg\hg\edo{

1509\hg\hg\edo{

1504\tp'\gets\vec{\MO{Match}}\;\tw\;\ttt\\

1510\tp'\gets\vec{\MO{Match}}\;\tw\;\ttt\\

papers/impl-paper/hll.tex+28−36

@@ -14,7 +14,7 @@ A full tutorial is available elsewhere \cite{idristutorial}.

14\subsection{Preliminaries}

16\Idris{} defines several primitive types: fixed width integers

17−\tTC{Int}, arbitrary width integers \tTC{Integer}, and

17+\tTC{Int}, arbitrary width integers \tTC{Integer},

18\tTC{Float} for numeric operations, \tTC{Char} and \tTC{String} for

19text manipulation, and \tTC{Ptr} which represents foreign pointers.

20There are also several data types declared in the library, including

@@ -46,7 +46,7 @@ being, in general, undecidable for languages with dependent types.

46A module declaration also opens a \remph{namespace}. The fully qualified names

47declared in this module are \texttt{Main.x} and \texttt{Main.main}.

49−\subsection{Types and Functions}

49+\subsection{Data Types}

51Data types may be declared in a similar way to Haskell data types, with a

52similar syntax. For example, Peano natural numbers and lists

@@ -83,7 +83,16 @@ is \emph{indexed} over \tTC{Nat} and \emph{parameterised} by a type.

83The distinction between parameters and indices is that a parameter is fixed

84across an entire data structure, whereas an index may vary.

85Note that constructor names may be overloaded (such as \texttt{Nil} and

86−\texttt{(::)} here) provided that they are declared in separate namespaces.

86+\texttt{(::)} here) provided that they are declared in separate

87+namespaces.

88+

89+\textbf{Remark:} In the library, \texttt{List} is declared in a module

90+\texttt{Prelude.List}, and \texttt{Vect} in a module \texttt{Prelude.Vect}, so

91+the fully qualified names of \texttt{Nil} are \texttt{Prelude.List.Nil} and

92+\texttt{Prelude.Vect.Nil}. They may be used qualified or unqualified; if

93+used unqualified the elaborator will disambiguate by type.

94+

95+\subsection{Functions}

88Functions are implemented by pattern matching. For example, the following

97Functions are implemented by pattern matching. For example, the following

89function defines concatenation of vectors, expressing in the type that

98function defines concatenation of vectors, expressing in the type that

@@ -107,15 +116,16 @@ be visible globally:

107\begin{SaveVerbatim}{revwhere}

116\begin{SaveVerbatim}{revwhere}

108

117

109reverse : List a -> List a

118reverse : List a -> List a

110−reverse xs = revAcc [] xs where

119+reverse xs = revAcc Nil xs where

111 revAcc : List a -> List a -> List a

120 revAcc : List a -> List a -> List a

112− revAcc acc [] = acc

121+ revAcc acc Nil = acc

113 revAcc acc (x :: xs) = revAcc (x :: acc) xs

122 revAcc acc (x :: xs) = revAcc (x :: acc) xs

114

123

115\end{SaveVerbatim}

124\end{SaveVerbatim}

116\useverb{revwhere}

125\useverb{revwhere}

117

126

118−\noindent

127+\subsubsection*{Totality checking}

128+

119Internally, \Idris{} programs are checked for \emph{totality} --- that they

129Internally, \Idris{} programs are checked for \emph{totality} --- that they

120produce an answer in finite time for all possible inputs --- but they are not

130produce an answer in finite time for all possible inputs --- but they are not

121\emph{required} to be total by default. Totality checking serves two

131\emph{required} to be total by default. Totality checking serves two

@@ -127,14 +137,14 @@ aggressively~\cite{Brady2003}.

127Totality checking can be enforced by using the \texttt{total} keyword.

137Totality checking can be enforced by using the \texttt{total} keyword.

128For example, the following definition is accepted:

138For example, the following definition is accepted:

129

139

130−\begin{SaveVerbatim}{vadd}

140+\begin{SaveVerbatim}{vaddt}

131

141

132total vAdd : Num a => Vect n a -> Vect n a -> Vect n a

142total vAdd : Num a => Vect n a -> Vect n a -> Vect n a

133−vAdd [] [] = []

143+vAdd Nil Nil = Nil

134vAdd (x :: xs) (y :: ys) = x + y :: vAdd xs ys

144vAdd (x :: xs) (y :: ys) = x + y :: vAdd xs ys

135

145

136\end{SaveVerbatim}

146\end{SaveVerbatim}

137−\useverb{vadd}

147+\useverb{vaddt}

138

148

139\noindent

149\noindent

140The elaborator can verify that this is total by checking that it covers all

150The elaborator can verify that this is total by checking that it covers all

@@ -149,8 +159,7 @@ checker is implemented independently of elaboration and type checking.

149\subsection{Implicit Arguments}

159\subsection{Implicit Arguments}

150

160

151In order to understand how \Idris{} elaborates to an underlying type theory,

161In order to understand how \Idris{} elaborates to an underlying type theory,

152−it is important first to understand the notion of \remph{implicit} arguments

162+it is important to understand the notion of \remph{implicit} arguments.

153−in types.

154To illustrate this, consider the finite sets:

163To illustrate this, consider the finite sets:

155

164

156\begin{SaveVerbatim}{findecl}

165\begin{SaveVerbatim}{findecl}

@@ -219,7 +228,7 @@ can still be given explicitly in applications, using the syntax

219

228

220\begin{SaveVerbatim}{vindexexp}

229\begin{SaveVerbatim}{vindexexp}

221

230

222−index {a=Int} {n=2} fO (2 :: 3 :: Nil)

231+index {a=Int} {n=2} fZ (2 :: 3 :: Nil)

223

232

224\end{SaveVerbatim}

233\end{SaveVerbatim}

225\useverb{vindexexp}

234\useverb{vindexexp}

@@ -241,7 +250,8 @@ gives a collection of overloaded operations which describe the interface for

241\remph{instances} of that class. \Idris{} classes follow Haskell~98 type

250\remph{instances} of that class. \Idris{} classes follow Haskell~98 type

242classes, except that multiple parameters are supported, and that classes can be

251classes, except that multiple parameters are supported, and that classes can be

243parameterised by \remph{any} value, not just types\footnote{Hence we refer to

252parameterised by \remph{any} value, not just types\footnote{Hence we refer to

244−them as \remph{classes} rather than \remph{type classes}.}.

253+them as \remph{classes} generally, rather than \remph{type classes}

254+specifically.}.

245

255

246A simple example is the \texttt{Show} class, which is defined in the

256A simple example is the \texttt{Show} class, which is defined in the

247library and provides an interface for converting values to \texttt{String}s:

257library and provides an interface for converting values to \texttt{String}s:

@@ -286,9 +296,10 @@ instance Show a => Show (Vect n a) where

286\useverb{showvec}

296\useverb{showvec}

287

297

288\noindent

298\noindent

289−Classes can also be extended. A logical next step from an equality relation \texttt{Eq}

299+Classes can also be extended. A logical next step from an equality relation

290−is to define an ordering relation \texttt{Ord}. We can define an \texttt{Ord} class

300+\texttt{Eq} for example is to define an ordering relation \texttt{Ord}. We can

291−which inherits methods from \texttt{Eq} as well as defining some of its own:

301+define an \texttt{Ord} class which inherits methods from \texttt{Eq} as well as

302+defining some of its own:

292

303

293\begin{SaveVerbatim}{ord}

304\begin{SaveVerbatim}{ord}

294

305

@@ -362,25 +373,6 @@ expressions to avoid the need to write auxiliary functions. It will

362

373

363\subsubsection{The \texttt{with} rule}

374\subsubsection{The \texttt{with} rule}

364

375

365−Since types can depend on values, the form of some arguments can be determined

366−by the value of others. For example, if we were to write down the implicit

367−length arguments to \texttt{(++)}, we would see that the form of the length argument was

368−determined by whether the vector was empty or not:

369−

370−\begin{SaveVerbatim}{appdep}

371−

372−(++) : Vect n a -> Vect m a -> Vect (n + m) a

373−(++) {n=O} [] [] = []

374−(++) {n=S k} (x :: xs) ys = x :: xs ++ ys

375−

376−\end{SaveVerbatim}

377−\useverb{appdep}

378−

379−\noindent

380−If \texttt{n} was a successor in the \texttt{[]} case, or zero in the

381−\texttt{::} case, the definition

382−would not be well typed.

383−

384Often, matching is required on the result of an intermediate computation

376Often, matching is required on the result of an intermediate computation

385with a dependent type.

377with a dependent type.

386\Idris{} provides a construct for this, the \texttt{with} rule,

378\Idris{} provides a construct for this, the \texttt{with} rule,

@@ -388,7 +380,7 @@ inspired by views in \Epigram~\cite{McBride2004a},

388which takes account of the

380which takes account of the

389fact that matching on a value in a dependently typed language can affect what

381fact that matching on a value in a dependently typed language can affect what

390is known about the forms of other values.

382is known about the forms of other values.

391−

383+%

392For example, a \texttt{Nat} is either even or odd.

384For example, a \texttt{Nat} is either even or odd.

393If it is even it will

385If it is even it will

394be the sum of two equal \texttt{Nat}s. Otherwise, it is the sum of two equal \texttt{Nat}s

386be the sum of two equal \texttt{Nat}s. Otherwise, it is the sum of two equal \texttt{Nat}s

papers/impl-paper/impldtp.tex+6−7

@@ -1,3 +1,4 @@

1+\RequirePackage{amsmath}

1\documentclass{jfp1}

2\documentclass{jfp1}

2%\documentclass[acmtoplas]{acmtrans2m}

3%\documentclass[acmtoplas]{acmtrans2m}

@@ -10,14 +11,13 @@

10\usepackage{epsfig}

11\usepackage{epsfig}

11%\usepackage{path}

12%\usepackage{path}

12\usepackage{url}

13\usepackage{url}

13−%\usepackage{amsmath}

14\usepackage{fancyvrb}

15−\usepackage{todonotes}

17\newenvironment{template}{\sffamily}

16\newenvironment{template}{\sffamily}

19%\usepackage{graphics,epsfig}

18%\usepackage{graphics,epsfig}

20\usepackage{stmaryrd}

19\usepackage{stmaryrd}

20+\usepackage{amsmath}

22\input{./macros.ltx}

23\input{./library.ltx}

@@ -80,11 +80,10 @@ language implementations. In this paper, I describe the implementation of

80and as such provides high level concepts such as implicit syntax,

81type classes and \texttt{do} notation.

82I describe the high level language and the underlying type theory, and present

83−a method for \emph{elaborating} concrete high level syntax with implicit

83+a tactic based method for \emph{elaborating} concrete high level syntax with

84−arguments and type classes into a fully explicit type theory. Furthermore,

84+implicit arguments and type classes into a fully explicit type theory.

85−I show how this method,

85+Furthermore, I show how this method facilitates the implementation of new high

86−based on a domain specific language embedded in Haskell, facilitates the

87−implementation of new high level language constructs.

86+level language constructs.

89%I describe the implementation of a dependently typed functional

88%I describe the implementation of a dependently typed functional

90%programming language, \Idris{}. Much has been written about various

89%programming language, \Idris{}. Much has been written about various

papers/impl-paper/intro.tex+54−26

@@ -27,8 +27,8 @@ By \emph{full} dependent types, we mean that there is no restriction on which

27values may appear in types. It is important for the sake of usability of a

28programming language to provide a notation which allows programmers to express

29high level concepts in a natural way. Taking Haskell as a starting point means

30−that \Idris{} offers a variety of high level structures such as type classes,

30+that \Idris{} offers a variety of high level structures such as type

31−\texttt{do}-notation, primitive types and monadic I/O, for example.

31+classes, \texttt{do}-notation, primitive types and monadic I/O, for example.

32Furthermore, a goal of \Idris{} is to support high level domain specific

33language implementation, providing appropriate notation for \emph{domain

34experts} and \emph{systems programmers}, who should not be required to be type

@@ -40,9 +40,9 @@ How can we achieve both of these goals?

40This paper describes a method for elaborating a high level dependently typed

41functional programming language to a low level core based on dependent

42type theory. The method involves building an elaboration monad which captures

43−the state of incomplete programs and a collection of \emph{tactics} for

43+the state of incomplete programs and a collection of \emph{tactics} used by the

44−refining programs, directed by high level syntax. As we shall see,

44+machine to refine programs, directed by high level syntax. As we shall see,

45−this method allows higher level language constructs to be constructed in a

45+this method allows higher level language constructs to be elaborated in a

46straightforward manner, without compromising the simplicity of the underlying

47type theory.

@@ -59,22 +59,50 @@ The primary contribution of this paper is a tactic based method for translating

59programs in a high level dependently typed programming language to a small core

60type theory, \TT{}, based on UTT \cite{luo1994}. The paper describes the

61structure of an elaboration monad capturing proof and system state, and

62−introduces a collection of \remph{tactics} for manipulating incomplete

62+introduces a collection of \remph{tactics} which the machine uses to

63−programs. Secondly, the paper gives a detailed description of the core type

63+manipulate incomplete programs. Secondly, the paper gives a detailed

64−theory used by \Idris{}, including a full description of the typing rules.

64+description of the core type theory used by \Idris{}, including a full

65−Finally, through describing the specific tactics, the paper shows how to extend

65+description of the typing rules. Finally, through describing the specific

66+tactics, the paper shows how to extend \Idris{} with higher level features.

66−\Idris{} with higher level features. While we apply these ideas to \Idris{}

67+While we apply these ideas to \Idris{} specifically, the method for term

67−specifically, the method for term construction is equally applicable to other

68+construction is equally applicable to other typed programming languages, and

68−typed programming languages, and indeed the tactics themselves are applicable

69+indeed the tactics themselves are applicable to any high level language which

69−to any high level language which can be explained in terms of \TT{}.

70+can be explained in terms of \TT{}.

70−

71+

71−The paper is structured as follows: Section \ref{sect:hll} gives an overview of

72+\subsection{Outline}

72−programming in \Idris{}, introducing the high level constructs which will be

73+

74+Translating an \Idris{} source program to an executable proceeds through several

75+phases, illustrated below:

76+

77+\begin{center}

78+\DM{

79+\mbox{\Idris{}}

80+\;

81+\xrightarrow{\mathrm{ (desugaring) }}

82+\;

83+\mbox{\IdrisM{}}

84+\;

85+\xrightarrow{\mathrm{ (elaboration) }}

86+\;

87+\mbox{\TT{}}

88+\;

89+\xrightarrow{\mathrm{ (compilation) }}

90+\;

91+\mbox{Executable}

92+}

93+\end{center}

94+

95+\noindent

96+The main focus of this paper is the elaboration phase, which translates

97+a desugared language \IdrisM{} into a core language \TT{}. In order to put

98+this into its proper context, I give an overview of the high level language

99+\Idris{} in Section \ref{sect:hll} and explain the core language \TT{} and

73−translated to the core language; Section \ref{sect:typechecking} describes the

100+its typing rules in Section \ref{sect:typechecking};

74−core language \TT{} and its typing rules, covering expressions, data types

75−and pattern matching; Section \ref{sect:elaboration} describes the method

101+Section \ref{sect:elaboration} describes the elaboration process itself,

76−for translating \Idris{} to \TT{}, beginning with a restricted language

102+beginning with a tactic based system for constructing

77−\IdrisM{} before extending to higher level features; Section

103+\TT{} programs, then introducing the desugared language \IdrisM{} and

104+showing how this is translated into \TT{} using tactics;

105+Section

78\ref{sect:delab} describes the process for translating \TT{} back to \Idris{}

106\ref{sect:delab} describes the process for translating \TT{} back to \Idris{}

79and properties of the translation; finally,

107and properties of the translation; finally,

80Section \ref{sect:related} discusses related work and Section \ref{sect:conclusion}

108Section \ref{sect:related} discusses related work and Section \ref{sect:conclusion}

@@ -110,7 +138,7 @@ elements of vectors of the same length:

110\begin{SaveVerbatim}{vadd}

138\begin{SaveVerbatim}{vadd}

111

139

112vAdd : Num a => Vect n a -> Vect n -> Vect n a

140vAdd : Num a => Vect n a -> Vect n -> Vect n a

113−vAdd [] [] = []

141+vAdd Nil Nil = Nil

114vAdd (x :: xs) (y :: ys) = x + y :: vAdd xs ys

142vAdd (x :: xs) (y :: ys) = x + y :: vAdd xs ys

115

143

116\end{SaveVerbatim}

144\end{SaveVerbatim}

@@ -120,16 +148,16 @@ vAdd (x :: xs) (y :: ys) = x + y :: vAdd xs ys

120This illustrates some basic features of \Idris{}:

148This illustrates some basic features of \Idris{}:

121

149

122\begin{itemize}

150\begin{itemize}

123−\item A single colon is used for type signatures, and a double colon for the

124−cons operator, emphasising the importance of types.

125\item Functions are defined by pattern matching, with a top level type signature.

151\item Functions are defined by pattern matching, with a top level type signature.

126Names which are free in the type signature (\texttt{a} and \texttt{n}) here

152Names which are free in the type signature (\texttt{a} and \texttt{n}) here

127are implicitly bound.

153are implicitly bound.

128\item The type system ensures that both input vectors are the same length (\texttt{n})

154\item The type system ensures that both input vectors are the same length (\texttt{n})

129and have the same element type (\texttt{a}), and that the element type and length

155and have the same element type (\texttt{a}), and that the element type and length

130are preserved in the output vector.

156are preserved in the output vector.

131−\item Functions can be overloaded using \remph{type classes}. Here, the element type

157+\item Functions can be overloaded using \remph{classes}. Here, the element type

132of the vector \texttt{a} must be numeric and therefore supports the \texttt{+} operator.

158of the vector \texttt{a} must be numeric and therefore supports the \texttt{+} operator.

159+\item A single colon is used for type signatures, and a double colon for the

160+cons operator, emphasising the importance of types.

133\end{itemize}

161\end{itemize}

134

162

135\noindent

163\noindent

@@ -137,7 +165,7 @@ of the vector \texttt{a} must be numeric and therefore supports the \texttt{+} o

137with dependent types, augmented with algebraic data types and pattern matching.

165with dependent types, augmented with algebraic data types and pattern matching.

138\TT{} programs are fully explicitly typed, including the names \texttt{a} and \texttt{n}

166\TT{} programs are fully explicitly typed, including the names \texttt{a} and \texttt{n}

139in the type signature, and the names bound in each pattern match clause.

167in the type signature, and the names bound in each pattern match clause.

140−Type classes are also made explicit.

168+Classes are also made explicit.

141The \TT{} translation of \texttt{vAdd} is:

169The \TT{} translation of \texttt{vAdd} is:

142

170

143\DM{

171\DM{

papers/impl-paper/macros.ltx+2−2

@@ -246,7 +246,7 @@

246\newcommand{\MyWith}[1]{\multicolumn{2}{l}{|\;#1}}

247\newcommand{\Byr}[1]{\;\RW{by}\; #1}

248

249−\newcommand{\Bar}{|}

249+\renewcommand{\Bar}{|}

250\newcommand{\Bart}{\settowidth{\GapLength}{$\Bar$}%

251 \raisebox{6pt}[0pt][0pt]{$\Bar$}%

252 \hspace*{-1\GapLength}%

@@ -276,7 +276,7 @@

276\newcommand{\As}[2]{#1 \:\RW{as}\: #2}

277\newcommand{\nhole}{\Box}

278\newcommand{\turq}{\:\vdash_?\:}

279−\newcommand{\split}{\;\lhd\;}

279+\renewcommand{\split}{\;\lhd\;}

280\newcommand{\CType}[2]{\{#1 \split\; #2\}}

281\newcommand{\CC}[2]{(#1)\:#2}

282\newcommand{\UP}[2]{#1 | \{#2\}}

papers/impl-paper/typechecking.tex+54−24

@@ -94,9 +94,19 @@ names may reduce.

95\label{sect:evaluation}

97+There are two distinct phases in which \TT{} evaluation occurs, namely

98+\demph{compile-time} and \demph{run-time}. Compile-time evaluation is primarily

99+to support type-checking, in which equivalence of two terms (or types) is

100+determined by comparing their normal forms. It is important that terms are

101+strongly normalising at compile-time, so any pattern matching definition which

102+is not guaranteed to be total does not reduce. In this section we discuss

103+compile-time evaluation; run-time evaluation differs in that there is no

104+reduction under binders, types and duplicated values have been

105+erased~\cite{Brady2003}, and non-normalising definitions may reduce.

106+

97−Evaluation of \TT{} is defined by contraction schemes, given in Figure

107+Compile-time evaluation of \TT{} is defined by contraction schemes, given in

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

108+Figure \ref{ttcontract}. \demph{Contraction}, relative to a context $\Gamma$,

99−by one of the following schemes:

109+is given by one of the following schemes:

100

110

101\begin{itemize}

111\begin{itemize}

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

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

@@ -267,12 +277,11 @@ defined collection of algebraic data types which can be parameterised over

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

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

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

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

269as

279as

270−follows, using vector notation, $\tx$, to indicate a

280+follows:

271−sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$):

272

281

273\DM{

282\DM{

274\AR{

283\AR{

275−\Data\hg\TC{T}\;(\tx\Hab\ttt)\Hab\vt\hg\Where\hg

284+\Data\hg\TC{T}\Hab\vt\hg\Where\hg

276\DC{D}_1\Hab\vt\;\mid\;\ldots\;\mid\;\DC{D}_n\Hab\vt

285\DC{D}_1\Hab\vt\;\mid\;\ldots\;\mid\;\DC{D}_n\Hab\vt

277}

286}

278}

287}

@@ -280,7 +289,10 @@ sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$):

280A constructor $\TC{D}$ of a family $\TC{T}$ must return a value in the family

289A constructor $\TC{D}$ of a family $\TC{T}$ must return a value in the family

281$\TC{T}$.

290$\TC{T}$.

282It may take recursive arguments in the family $\TC{T}$ which may be

291It may take recursive arguments in the family $\TC{T}$ which may be

292+higher order.

293+Using vector notation, $\tx$, to indicate a

294+sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$),

283−higher order. That is, recursive arguments have types of the form

295+recursive arguments have types of the form

284

296

285\DM{

297\DM{

286\all{\vx_1}{\vS_1}\SC\ldots\all{\vx_n}{\vS_n}\SC\TC{T}\:\ty

298\all{\vx_1}{\vS_1}\SC\ldots\all{\vx_n}{\vS_n}\SC\TC{T}\:\ty

@@ -301,8 +313,8 @@ For example, the \Idris{} data type \tTC{Nat} would be declared in \TT{} as foll

301}

313}

302

314

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

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

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

316+across a structure) and a number of indices, given by the type. For example,

305−example, the \TT{} equivalent of \tTC{List} is parameterised over its element type:

317+the \TT{} equivalent of \tTC{List} is parameterised over its element type:

306

318

307\DM{

319\DM{

308\AR{

320\AR{

@@ -316,7 +328,7 @@ example, the \TT{} equivalent of \tTC{List} is parameterised over its element ty

316}

328}

317

329

318Types can be

330Types can be

319−parameterised over values. Using this, we can declare the type of

331+parameterised or indexed over values. Using this, we can declare the type of

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

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

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

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

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

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

@@ -362,7 +374,7 @@ and the types of each side must be convertible. Additionally, the

362left hand side must take the form of $\FN{f}$ applied to a number of \TT{} expressions,

374left hand side must take the form of $\FN{f}$ applied to a number of \TT{} expressions,

363and the number of arguments must be the same in each clause. The right hand

375and the number of arguments must be the same in each clause. The right hand

364sides may include applications of $\FN{f}$, i.e. pattern matching definitions may

376sides may include applications of $\FN{f}$, i.e. pattern matching definitions may

365−be recursive. Termination analysis is implemented separately. The validity of a pattern

377+be recursive. The validity of a pattern

366clause is defined by the following rule:

378clause is defined by the following rule:

367

379

368\DM{

380\DM{

@@ -375,14 +387,19 @@ clause is defined by the following rule:

375}

387}

376}

388}

377

389

390+Patterns are separated into the accessible patterns (variables and constructor

391+forms which may be inspected) and inaccessible patterns, following

392+Agda~\cite{norell2007thesis} then implemented by compilation into case

393+trees~\cite{Augustsson1985}. Non-terminating definitions are permitted, but do

394+not reduce at compile-time, which means in particular that they cannot be used

395+to construct proofs.

396+Termination analysis is implemented separately.

397+

378A valid pattern matching definition effectively extends \TT{} with a new

398A valid pattern matching definition effectively extends \TT{} with a new

379constant, with the given type (extending the initial typing rules given in

399constant, with the given type (extending the initial typing rules given in

380Section \ref{sect:typerules}) and reduction behaviour (extending the initial

400Section \ref{sect:typerules}) and reduction behaviour (extending the initial

381reduction rules given in Section \ref{sect:evaluation}).

401reduction rules given in Section \ref{sect:evaluation}).

382−Patterns are separated into the accessible patterns (variables and constructor

402+

383−forms which may be inspected) and inaccessible patterns, following

384−Agda~\cite{norell2007thesis} then implemented by compilation into case

385−trees~\cite{Augustsson1985}.

386

403

387% \subsubsection{Semantics}

404% \subsubsection{Semantics}

388%

405%

@@ -532,26 +549,37 @@ trees~\cite{Augustsson1985}.

532\mbox{then} & \Gamma_0,\Gamma_1\proves\vs\Hab\vS\\

549\mbox{then} & \Gamma_0,\Gamma_1\proves\vs\Hab\vS\\

533(\mbox{where} & \mathcal{B}(\vx, \vT) \proves \vx\Hab\vT)

550(\mbox{where} & \mathcal{B}(\vx, \vT) \proves \vx\Hab\vT)

534\end{array}

551\end{array}

552+\medskip

553+\\

554+\mbox{\textbf{Strong normalisation}} &

555+\begin{array}{ll}

556+\mbox{If} & \Gamma\proves\vt\Hab\vT\\

557+\mbox{then} & \vt\:\mbox{is strongly normalising}\\

558+\end{array}

535\\

559\\

536\end{array}

560\end{array}

537}

561}

538{Metatheoretic properties of \TT{}}

562{Metatheoretic properties of \TT{}}

539{metatheory}

563{metatheory}

540

564

541−We conjecture that \TT{} respects the usual metatheoretic properties, as shown in

565+We conjecture that \TT{} respects the usual metatheoretic properties,

566+as shown in

542Figure \ref{metatheory}. Specifically: the \demph{Church-Rosser} property

567Figure \ref{metatheory}. Specifically: the \demph{Church-Rosser} property

543(i.e. that distinct reduction sequences lead to the same normal form);

568(i.e. that distinct reduction sequences lead to the same normal form);

544\demph{subject reduction} (i.e. that computation preserves type); the

569\demph{subject reduction} (i.e. that computation preserves type); the

545\demph{cut} property (i.e. that $\RW{let}$-bound terms may be substituted into

570\demph{cut} property (i.e. that $\RW{let}$-bound terms may be substituted into

546their scope); and \demph{strengthening} (i.e. that removing unused definitions

571their scope); and \demph{strengthening} (i.e. that removing unused definitions

547from scope does not affect type checking).

572from scope does not affect type checking).

573+\demph{Strong normalisation} holds at compile-time because pattern matching

574+definitions which cannot be shown to be terminating do not have compile-time

575+reduction behaviour.

548

576

549−One property which is noticeably absent is \demph{strong normalisation}.

577+%One property which is noticeably absent is \demph{strong normalisation}.

550−Although desirable to preserve termination and decidability of type checking,

578+%Although desirable to preserve termination and decidability of type checking,

551−we allow diverging terms for pragmatic reasons as \Idris{} is primarily a

579+%we allow diverging terms for pragmatic reasons as \Idris{} is primarily a

552−programming language rather than a theorem prover. Nevertheless, we do

580+%programming language rather than a theorem prover. Nevertheless, we do

553−\emph{check} for totality in order to be sure which terms are safe to

581+%\emph{check} for totality in order to be sure which terms are safe to

554−evaluate at compile time.

582+%evaluate at compile time.

555

583

556\subsection{Totality checking}

584\subsection{Totality checking}

557

585

@@ -607,7 +635,8 @@ also treated as an implicit argument, to which we give the name \texttt{c}:

607

635

608\begin{SaveVerbatim}{vAddImp}

636\begin{SaveVerbatim}{vAddImp}

609

637

638+vAdd : (a : _) -> (n : _) ->

610−vAdd : (a : _) -> (n : _) -> Num a -> Vect n a -> Vect n a -> Vect n a

639+ Num a -> Vect n a -> Vect n a -> Vect n a

611vAdd _ _ c (Nil _) (Nil _) = (Nil _)

640vAdd _ _ c (Nil _) (Nil _) = (Nil _)

612vAdd _ _ c ((::) _ _ x xs) ((::) _ _ y ys)

641vAdd _ _ c ((::) _ _ x xs) ((::) _ _ y ys)

613 = (::) _ _ ((+) _ x y) (vAdd _ _ _ xs ys)

642 = (::) _ _ ((+) _ x y) (vAdd _ _ _ xs ys)

@@ -621,7 +650,8 @@ algorithm:

621

650

622\begin{SaveVerbatim}{vAddImpSolve}

651\begin{SaveVerbatim}{vAddImpSolve}

623

652

653+vAdd : (a : Type) -> (n : Nat) ->

624−vAdd : (a : Type) -> (n : Nat) -> Num a -> Vect n a -> Vect n a -> Vect n a

654+ Num a -> Vect n a -> Vect n a -> Vect n a

625vAdd a O c (Nil a) (Nil a) = Nil a

655vAdd a O c (Nil a) (Nil a) = Nil a

626vAdd a (S k) c ((::) a k x xs) ((::) a k y ys)

656vAdd a (S k) c ((::) a k x xs) ((::) a k y ys)

627 = (::) a k ((+) c x y) (vAdd a k c xs ys)

657 = (::) a k ((+) c x y) (vAdd a k c xs ys)