8000794 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Final (I hope!) implementation paper tinkering

8000794Edwin Brady13 years ago

CHANGELOG+1

compare with master

unifiedsplit

@@ -12,6 +12,7 @@ New in 0.9.10:

12Internal changes

14* New module/dependency tree checking

15+* Compiling Nat via GMP integers

16New in 0.9.9:

17New in 0.9.9:

17-------------

18-------------

papers/impl-paper/conclusions.tex+21−21

@@ -2,13 +2,13 @@

3\label{sect:related}

5−Dependently typed programming languages have become more prominent in recent

5+Dependently-typed programming languages have become more prominent in recent

6years as tools for verifying software correctness, and several experimental

7languages are being developed, in particular Agda \cite{norell2007thesis},

8Epigram \cite{McBride2004a,Levitation2010} and Trellys \cite{Kimmell2012}.

9Furthermore, recent extensions to Haskell~\cite{Vytiniotis2011}, implemented in the

10Glasgow Haskell Compiler, are bringing more of the power of dependent types to

11−Haskell. The problem of refining high level syntax to a core type theory also

11+Haskell. The problem of refining high-level syntax to a core type theory also

12applies to theorem provers based on dependent types such as

13Coq~\cite{Bertot2004} and Matita~\cite{Asperti2011}.

@@ -20,7 +20,7 @@ Types are checked using an inference algorithm

20inference engine independent of the constraint

21system, and a constraint solver for $X$. An additional difficulty faced by

22Haskell, and hence any extensions, is the desire to support type \emph{inference}, in

23−which principal types may be inferred for top level functions. We have avoided

23+which principal types may be inferred for top-level functions. We have avoided

24such difficulties since, in general, type

25inference is undecidable for full dependent types. Indeed, it is not clear

26that type inference is even desirable in many cases, as programmers

@@ -32,14 +32,14 @@ inference.

32An earlier implementation of \Idris{} was built on the \Ivor{} proof engine

33\cite{Brady2006b}. This implementation differed in one important way --- unlike

34the present implementation, there was limited separation between the type

35−theory and the high level language. The type theory itself supported implicit

35+theory and the high-level language. The type theory itself supported implicit

36−syntax and unification, with high level constructs such as the \texttt{with}

36+syntax and unification, with high-level constructs such as the \texttt{with}

37rule implemented directly. Two important disadvantages were found with this

38approach, however: firstly, the type checker is much more complicated when

39combined with unification, making it harder to maintain; secondly, adding new

40−high level features requires the type checker to support those features

40+high-level features requires the type checker to support those features

41directly. In contrast, elaboration by tactics gives a clean separation between

42−the low level and high level languages, and results in programs in a core

42+the low-level and high-level languages, and results in programs in a core

43type theory which is separately checkable, perhaps even by an independently

44written checker which implements the \TT{} rules directly.

@@ -48,12 +48,12 @@ type directed approach, maintaining a set of yet to be solved unification

48problems and relying on a small kernel, similar to the approach we now take

49with \Idris{}, However, their approach uses refinement rules rather than

50tactics. This leads to good error messages though it is not clear how

51−easy it would be to extend to additional high level language features, unlike

51+easy it would be to extend to additional high-level language features, unlike

52−the tactic based approach.

52+the tactic-based approach.

54The Agda implementation is based on a type theory with

55implicit syntax and pattern matching --- Norell gives an algorithm for type checking

56−a dependently typed language with pattern matching and metavariables

56+a dependently-typed language with pattern matching and metavariables

57\cite{norell2007thesis}. Unlike the present \Idris{} implementation, metavariables

58and implicit arguments are part of the type theory. This has the advantage that

59implicit arguments can be used more freely (for example, in higher order

@@ -84,7 +84,7 @@ implementation of extra machinery for constructor manipulation

85In this paper, I have given an overview of the programming language \Idris{},

86and its core type theory \TT{}, giving a detailed algorithm for translating

87−high level programs into \TT{}.

87+high-level programs into \TT{}.

88\TT{} itself is deliberately small and simple, and the design has deliberately

89resisted innovation so that we can rely on existing metatheoretic properties

90being preserved. The kernel of the \Idris{} implementation consists of a type checker

@@ -94,11 +94,11 @@ in under 1000 lines of Haskell code. It is important that this kernel remains sm

94the correctness of the underlying type system, and keeping the implementation small

95reduces the possibility of errors.

97−The approach we have taken to implementing the high level language,

97+The approach we have taken to implementing the high-level language,

98implementing an elaboration monad with tactics for program construction, allows

99us to build programs on top of a small and unchanging kernel, rather than

100extending the core language to deal with implicit syntax, unification and type

101−classes. High level \Idris{} features are implemented by describing the

101+classes. High-level \Idris{} features are implemented by describing the

102corresponding sequence of tactics to build an equivalent program in \TT{}, via

103a development calculus of incomplete terms, \TTdev{}. A significant advantage

104we have found with this approach is that higher level features can easily be

@@ -108,19 +108,19 @@ several features:

108

109\begin{itemize}

110\item \textbf{Type classes}: A dictionary is merely a record containing the

111−functions which implement a type class instance. Since we have a tactic based

111+functions which implement a type class instance. Since we have a tactic-based

112refinement engine, we can implement type class resolution as a tactic.

113\item \textbf{\texttt{where} clauses}: We have access to local variables and

114their types, so we can

115elaborate \texttt{where} clauses at the point of definition simply by lifting

116them to the top level.

117\item \textbf{\texttt{case} expressions}: Similar to \texttt{where} clauses,

118−these are implemented by lifting the branches out to a top level function.

118+these are implemented by lifting the branches out to a top-level function.

119\end{itemize}

120

121We do not need to make any changes to the core language type system in order to

122−implement these high level features.

122+implement these high-level features.

123−Other high level features such as dependent records, tuples and monad comprehensions

123+Other high-level features such as dependent records, tuples and monad comprehensions

124can be added equally easily --- and indeed have been added in the full implementation.

125Furthermore,

126since we have taken a tactic-based approach to elaborating \Idris{} to \TT{},

@@ -129,7 +129,7 @@ the possibility of implementing domain specific decision procedures, or

129implementing user defined tactics in a style similar to Coq's \texttt{Ltac}

130language \cite{Delahaye2000}. Although \TT{} is primarily intended as a core

131language for \Idris{}, its rich type system also means that it could be used

132−as a core language for other high level languages, especially when augmented

132+as a core language for other high-level languages, especially when augmented

133with primitive operators, and used to express additional properties of those

134languages.

135

@@ -152,16 +152,16 @@ The objective of this implementation of \Idris{} is to provide a platform

152for experimenting with realistic, general purpose programming with dependent

153types, by implementing a Haskell-like language augmented with \emph{full}

154dependent types.

155−In this paper, we have seen how such a high level language can be implemented

155+In this paper, we have seen how such a high-level language can be implemented

156by building on top of a small, well-understood, easy to reason about type

157theory.

158However, a programming language implementation is not an end in itself.

159Programming languages exist to support research and practice in many different

160domains. In future work, therefore, I plan to apply domain specific

161−language based techniques to realistic problems in important safety critical

161+language-based techniques to realistic problems in important safety critical

162domains such as security and network protocol design and implementation. In

163order to be successful, this will require a language which is expressive enough

164−to describe protocol specifications at a high level, and robust enough to

164+to describe protocol specifications at a high-level, and robust enough to

165guarantee correct implementation of those protocols. \Idris{}, I believe, is

166the right tool for this work.

167

papers/impl-paper/delab.tex+2−2

@@ -89,7 +89,7 @@ which arguments are implicit or constraint arguments:

89}

91\noindent

92−Using this, we define $\MO{Unelab}$ for top level declarations. For pattern

92+Using this, we define $\MO{Unelab}$ for top-level declarations. For pattern

93matching clauses reversing elaboration proceeds as follows, discarding the explicit

94pattern variable bindings and applying $\MO{UnelabType}$ to reconstruct

95the type declaration:

@@ -104,7 +104,7 @@ the type declaration:

104

105\noindent

106For data type declarations, reverse elaboration proceeds as follows, applying $\MO{UnelabType}$

107−for each of the top level type declarations:

107+for each of the top-level type declarations:

108

109\DM{

110\AR{

papers/impl-paper/elaboration.tex+33−30

@@ -8,23 +8,23 @@

9An \Idris{} program consists of a series of declarations --- data types,

10functions, classes and instances. In this section, we describe how these

11−high level declarations are translated into a \TT{} program consisting of

11+high-level declarations are translated into a \TT{} program consisting of

12inductive families and pattern matching function definitions. We will need to

13work at the \remph{declaration} level, and at the \remph{expression} level,

14defining the following meta-operations.

16\begin{itemize}

17\item $\ttinterp{\cdot}$, which builds a \TT{} expression from an \Idris{} expression.

18−\item $\MO{Elab}$, which processes a top level \Idris{} declaration by generating

18+\item $\MO{Elab}$, which processes a top-level \Idris{} declaration by generating

19one or more \TT{} declarations.

20−\item $\MO{TTDecl}$, which adds a top level \TT{} declaration.

20+\item $\MO{TTDecl}$, which adds a top-level \TT{} declaration.

21\end{itemize}

24\subsection{The Development Calculus \TTdev}

26−\TT{} expressions are built by using high level \Idris{} expressions to

26+\TT{} expressions are built by using high-level \Idris{} expressions to

27−direct a tactic based theorem prover, which builds the \TT{} expressions

27+direct a tactic-based theorem prover, which builds the \TT{} expressions

28step by step, by refinement. In order to build expressions in this way,

29the type theory needs to support

30\remph{incomplete} terms, and a method for term construction.

@@ -40,7 +40,7 @@ These extensions are given in Figure \ref{ttdev}.

40The \remph{guess} binding is

41similar to a $\LET$ binding, but without any computational force,

42i.e. there are no reduction rules for guess bindings.

43−Using binders to represent holes is useful in a dependently typed setting since

43+Using binders to represent holes is useful in a dependently-typed setting since

44one value may determine another. Attaching a guess to a binder ensures that

45instantiating one such variable also instantiates all of its dependencies.

46%The

@@ -87,12 +87,11 @@ instantiating one such variable also instantiates all of its dependencies.

88\label{sect:prfstate}

90−We will build expressions in \TT{} from high level \Idris{} expressions by

90+We will build expressions in \TT{} from high-level \Idris{} expressions by

91−creating a top level hole binding with the appropriate type, and refining it

91+creating a top-level hole binding with the appropriate type, and refining it

92according to the structure of the \Idris{} expression. Noting the Curry-Howard

93correspondence between programs and proofs, and the relationship between our

94−method for elaboration and tactic

95−based theorem proving, we refer to a development as a \emph{proof}.

94+method for elaboration and tactic-based theorem proving, we refer to a development as a \emph{proof}.

96A proof state is a tuple, $(\vC, \Delta, \ve, \vP, \vQ)$, containing:

95A proof state is a tuple, $(\vC, \Delta, \ve, \vP, \vQ)$, containing:

98\begin{itemize}

97\begin{itemize}

@@ -118,7 +117,7 @@ When the hole queue is empty, and there are no remaining unification

118problems, the proof term is complete.

117problems, the proof term is complete.

119

118

120Creating a \TT{} expression from an \Idris{} expression involves creating

119Creating a \TT{} expression from an \Idris{} expression involves creating

121−a new proof state, with an empty proof term, and using the high level definition

120+a new proof state, with an empty proof term, and using the high-level definition

122to direct the building of a final proof state, with a complete proof term.

121to direct the building of a final proof state, with a complete proof term.

123

122

124In the implementation, the proof state is captured in an elaboration monad,

123In the implementation, the proof state is captured in an elaboration monad,

@@ -890,7 +889,7 @@ a Coq proof script.

890

889

891\label{sect:sysstate}

890\label{sect:sysstate}

892

891

893−To elaborate \Idris{} programs we will build expressions from high level

892+To elaborate \Idris{} programs we will build expressions from high-level

894declarations of functions, data types and classes, and add the resulting

893declarations of functions, data types and classes, and add the resulting

895definitions to a global system state.

894definitions to a global system state.

896The system state is a tuple, $(\vC,\vA,\vI)$, containing:

895The system state is a tuple, $(\vC,\vA,\vI)$, containing:

@@ -1035,7 +1034,7 @@ arguments in types bound explicitly

1035(e.g. $\piimp{\va}{\_}\piimp{\vn}{\_}\TC{Vect}\;\vn\;\va$

1034(e.g. $\piimp{\va}{\_}\piimp{\vn}{\_}\TC{Vect}\;\vn\;\va$

1036instead of simply $\Vect\;\vn\;\va$).

1035instead of simply $\Vect\;\vn\;\va$).

1037Note that we separate implicit and type constraint bindings, to ensure that they

1036Note that we separate implicit and type constraint bindings, to ensure that they

1038−only appear in top level declarations.

1037+only appear in top-level declarations.

1039It is in general straightforward to

1038It is in general straightforward to

1040convert full \Idris{} to \IdrisM{} --- syntactic sugar is implemented by a

1039convert full \Idris{} to \IdrisM{} --- syntactic sugar is implemented by a

1041direct source transformation, and implicit arguments can be identified as the names

1040direct source transformation, and implicit arguments can be identified as the names

@@ -1091,10 +1090,7 @@ elaboration will fail.

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

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

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

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

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

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

1094−check means that the variable is a pattern variable\footnote{In Haskell,

1093+check means that the variable is a pattern variable:

1095−pattern variables are all lower case, so type checking can assume that a

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

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

1098

1094

1099\DM{

1095\DM{

1100\ttpinterp{\vx}\;\mq\;

1096\ttpinterp{\vx}\;\mq\;

@@ -1103,6 +1099,11 @@ name in a pattern may refer to a function, if forced by some dependency.}:

1103}

1099}

1104}

1100}

1105

1101

1102+In Haskell, for comparison,

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

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

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

1106+

1106We also need to elaborate \remph{placeholders}, which are subexpressions we expect to

1107We also need to elaborate \remph{placeholders}, which are subexpressions we expect to

1107solve by unification. In this case, we simply move on to the next hole in the queue, moving

1108solve by unification. In this case, we simply move on to the next hole in the queue, moving

1108the current hole to the end of the queue with $\MO{Unfocus}$:

1109the current hole to the end of the queue with $\MO{Unfocus}$:

@@ -1425,14 +1426,14 @@ the right hand side $\ve$ to use the lifted definitions, rather than the origina

1425\subsubsection{Elaborating the \texttt{with} rule}

1426\subsubsection{Elaborating the \texttt{with} rule}

1426

1427

1427The \texttt{with} rule allows \remph{dependent} pattern matching on intermediate values.

1428The \texttt{with} rule allows \remph{dependent} pattern matching on intermediate values.

1428−Translating this into \TT{} involves constructing an auxiliary top level

1429+Translating this into \TT{} involves constructing an auxiliary top-level

1429definition for

1430definition for

1430the intermediate pattern match. For example, recall \tFN{natToBin}:

1431the intermediate pattern match. For example, recall \tFN{natToBin}:

1431

1432

1432\useverb{natToBin}

1433\useverb{natToBin}

1433

1434

1434\noindent

1435\noindent

1435−This is equivalent to the following, using top level definitions only:

1436+This is equivalent to the following, using top-level definitions only:

1436

1437

1437\begin{SaveVerbatim}{natToBinw}

1438\begin{SaveVerbatim}{natToBinw}

1438

1439

@@ -1454,8 +1455,10 @@ natToBin' (S (j + j)) odd = True :: natToBin j

1454

1455

1455\noindent

1456\noindent

1456Additionally, the elaborator abstracts over the term being analysed in the type

1457Additionally, the elaborator abstracts over the term being analysed in the type

1457−of the generated auxiliary definition\footnote{This is sometimes referred to

1458+of the generated auxiliary definition

1459+%\footnote{This is sometimes referred to

1460+%as ``magic \texttt{with}''.}

1458−as ``magic \texttt{with}''.} and reorders the arguments as required.

1461+and reorders the arguments as required.

1459For example:

1462For example:

1460

1463

1461\begin{SaveVerbatim}{magicwith}

1464\begin{SaveVerbatim}{magicwith}

@@ -1533,7 +1536,7 @@ A $\iwith$ block in a clause for $\vx$

1533results in an auxiliary definition $\vx'$, where $\vx'$ is a fresh name,

1536results in an auxiliary definition $\vx'$, where $\vx'$ is a fresh name,

1534which takes an extra argument corresponding to the intermediate result which

1537which takes an extra argument corresponding to the intermediate result which

1535is to be matched.

1538is to be matched.

1536−$\MO{MatchWith}$ matches the left hand side of the top level definition against

1539+$\MO{MatchWith}$ matches the left hand side of the top-level definition against

1537each $\VV{pclause}$, using the result of the match to build each pattern clause

1540each $\VV{pclause}$, using the result of the match to build each pattern clause

1538for $\vx'$.

1541for $\vx'$.

1539The clauses in the with block must be of a specific form: they must have an initial

1542The clauses in the with block must be of a specific form: they must have an initial

@@ -1554,7 +1557,7 @@ Classes are implemented as dictionaries of functions for each instance,

1554following the implementation of first class type classes in Coq~\cite{Sozeau2008}.

1557following the implementation of first class type classes in Coq~\cite{Sozeau2008}.

1555Therefore, a class declaration elaborates to a record type containing all

1558Therefore, a class declaration elaborates to a record type containing all

1556of the functions in the class, and an instance is simply an instance of the

1559of the functions in the class, and an instance is simply an instance of the

1557−record. The methods are translated to top level functions which extract the

1560+record. The methods are translated to top-level functions which extract the

1558relevant function from the dictionary. For example, for the \texttt{Show}

1561relevant function from the dictionary. For example, for the \texttt{Show}

1559class, the \texttt{class} declaration is translated (in the elaborated code,

1562class, the \texttt{class} declaration is translated (in the elaborated code,

1560using the surface \Idris{} syntax for readability)

1563using the surface \Idris{} syntax for readability)

@@ -1585,7 +1588,7 @@ showNat = InstanceShow show' where

1585\end{SaveVerbatim}

1588\end{SaveVerbatim}

1586\useverb{shownatf}

1589\useverb{shownatf}

1587

1590

1588−The call to \tFN{show} in the body of the instance uses the top level \tFN{show}

1591+The call to \tFN{show} in the body of the instance uses the top-level \tFN{show}

1589function, with the instance resolved by the elaborator.

1592function, with the instance resolved by the elaborator.

1590Where instances have constraints, these constraints are passed on to

1593Where instances have constraints, these constraints are passed on to

1591the function declaration for the instance. For example, for \texttt{Show (List a)}:

1594the function declaration for the instance. For example, for \texttt{Show (List a)}:

@@ -1710,7 +1713,7 @@ defined instance:

1710Adding default definitions is straightforward: simply insert the default definition where

1713Adding default definitions is straightforward: simply insert the default definition where

1711there is a method missing in an \texttt{instance} declaration.

1714there is a method missing in an \texttt{instance} declaration.

1712

1715

1713−\textbf{Remark:} Here, we have added a higher level language construct

1716+Here, we have added a higher level language construct

1714(classes) simply by elaborating in terms of lower level language constructs

1717(classes) simply by elaborating in terms of lower level language constructs

1715(data types and functions). We achieve type class resolution by implementing a

1718(data types and functions). We achieve type class resolution by implementing a

1716tactic, $\MO{Instance}$. We can build several extensions this way because we

1719tactic, $\MO{Instance}$. We can build several extensions this way because we

@@ -1814,8 +1817,8 @@ dependent pattern matching definitions and expansion of implicit arguments

1814and classes. In order to make the language truly general purpose, however, we

1817and classes. In order to make the language truly general purpose, however, we

1815will need to add higher level extensions. Full \Idris{} is \IdrisM{} extended

1818will need to add higher level extensions. Full \Idris{} is \IdrisM{} extended

1816with \texttt{do}-notation, idiom brackets~\cite{McBride2007}, \texttt{case} expressions,

1819with \texttt{do}-notation, idiom brackets~\cite{McBride2007}, \texttt{case} expressions,

1817−pattern matching \texttt{let}, metavariables and tactic based theorem proving.

1820+pattern matching \texttt{let}, metavariables and tactic-based theorem proving.

1818−The majority of these extensions are straightforward transformations of high level

1821+The majority of these extensions are straightforward transformations of high-level

1819\Idris{} programs --- for example, \texttt{do}-notation can be reduced directly to

1822\Idris{} programs --- for example, \texttt{do}-notation can be reduced directly to

1820\IdrisM{} function applications. Some, however, require further support. In this section,

1823\IdrisM{} function applications. Some, however, require further support. In this section,

1821we complete the presentation of \IdrisM{} by extending it with metavariables

1824we complete the presentation of \IdrisM{} by extending it with metavariables

@@ -1877,7 +1880,7 @@ append_rec a m n x xs ys = app xs ys

1877\end{SaveVerbatim}

1880\end{SaveVerbatim}

1878\useverb{appendrec_def}

1881\useverb{appendrec_def}

1879

1882

1880−Elaborating a metavariable involves adding a new top level definition which is applied

1883+Elaborating a metavariable involves adding a new top-level definition which is applied

1881to all of the variables in local scope.

1884to all of the variables in local scope.

1882

1885

1883\DM{

1886\DM{

@@ -1894,8 +1897,8 @@ to all of the variables in local scope.

1894

1897

1895A \texttt{case} expression allows pattern matching on intermediate values. The difficulty

1898A \texttt{case} expression allows pattern matching on intermediate values. The difficulty

1896in elaborating \texttt{case} expressions is that \TT{} allows matching only on

1899in elaborating \texttt{case} expressions is that \TT{} allows matching only on

1897−\emph{top level} values. Elaborating a \texttt{case} expression, therefore,

1900+\emph{top-level} values. Elaborating a \texttt{case} expression, therefore,

1898−involves creating a new top level function standing for the expression, and applying it.

1901+involves creating a new top-level function standing for the expression, and applying it.

1899The natural

1902The natural

1900way to implement this is to use a metavariable. For example, we have already seen

1903way to implement this is to use a metavariable. For example, we have already seen

1901\texttt{lookup\_default}:

1904\texttt{lookup\_default}:

papers/impl-paper/hll.tex+10−9

@@ -39,8 +39,8 @@ main = putStrLn ("The answer is " ++ show x)

40\noindent

41Like Haskell, the main function is called \texttt{main}, and input and output

42−is managed with an \texttt{IO} monad. Unlike Haskell, however, \remph{all} top

42+is managed with an \texttt{IO} monad. Unlike Haskell, however, \remph{all}

43−level functions must have a type signature. This is due to type inference

43+top-level functions must have a type signature. This is due to type inference

44being, in general, undecidable for languages with dependent types.

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

@@ -62,7 +62,7 @@ data List a = Nil | (::) a (List a)

63\noindent

64A standard example of a \remph{dependent} type is the type of ``lists with

65−length'', conventionally called ``vectors'' in the dependently typed

65+length'', conventionally called ``vectors'' in the dependently-typed

66programming literature. In \Idris{}, vectors are declared as follows:

68\begin{SaveVerbatim}{vectdecl}

@@ -86,7 +86,7 @@ Note that constructor names may be overloaded (such as \texttt{Nil} and

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

87namespaces.

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

89+Note that in the library, \texttt{List} is declared in a module

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

91the 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

@@ -241,17 +241,18 @@ overloaded in an ad-hoc manner and resolved according to the context in which

241they are used. This is mostly for convenience, to eliminate the need to

242decorate constructor names in similarly structured data types, and eliminate

243explicit qualification of ambiguous names where only one is well-typed --- this

244−is especially useful for disambiguating record field names\footnote{Records are

244+is especially useful for disambiguating record field names, although records

245−however beyond the scope of this paper}.

245+are beyond the scope of this paper.

246

247Secondly, \Idris{} implements \remph{classes}, following Haskell's type

248classes. This allows a more principled approach to overloading --- a class

249gives a collection of overloaded operations which describe the interface for

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

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

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

252+parameterised by \remph{any} value, not just types.

253+Hence we refer to

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

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

254−specifically.}.

255+specifically.

255

256

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

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

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

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

@@ -378,7 +379,7 @@ with a dependent type.

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

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

379inspired by views in \Epigram~\cite{McBride2004a},

380inspired by views in \Epigram~\cite{McBride2004a},

380which takes account of the

381which takes account of the

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

382+fact that matching on a value in a dependently-typed language can affect what

382is known about the forms of other values.

383is known about the forms of other values.

383%

384%

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

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

papers/impl-paper/impldtp.tex+10−10

@@ -70,20 +70,20 @@ KY16 9SX, UK}

70\maketitle

72\begin{abstract}

73−Many components of a dependently typed programming language are by now well

73+Many components of a dependently-typed programming language are by now well

74understood, for example the underlying type theory, type checking, unification and

75−evaluation. How to combine these components into a realistic and usable high

75+evaluation. How to combine these components into a realistic and usable

76−level language is, however, folklore, discovered anew by successive

76+high-level language is, however, folklore, discovered anew by successive

77−language implementations. In this paper, I describe the implementation of

77+language implementators. In this paper, I describe the implementation of

78−\Idris{}, a new dependently typed functional programming language.

78+\Idris{}, a new dependently-typed functional programming language.

79\Idris{} is intended to be a \emph{general purpose} programming language

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

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

81type classes and \texttt{do} notation.

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

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

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

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

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

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

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

86−level language constructs.

86+high-level language constructs.

88%I describe the implementation of a dependently typed functional

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

papers/impl-paper/intro.tex+20−20

@@ -1,6 +1,6 @@

1\section{Introduction}

3−Dependently typed programming languages, such as Agda \cite{norell2007thesis}

3+Dependently-typed programming languages, such as Agda \cite{norell2007thesis}

4and Coq \cite{Bertot2004}, have emerged in recent years as a promising approach

5to ensuring the correctness of software. Type checking ensures a program has

6the intended meaning; \emph{dependent} types, where types may be predicated

@@ -26,10 +26,10 @@ language, has no such limitation, essentially asking the question:

26By \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

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

29+high-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

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

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

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

32+Furthermore, 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

35theorists in order to solve programming problems. Nevertheless, it is

@@ -37,26 +37,26 @@ important for the sake of correctness of the language implementation to have a

37well-defined core language with well-understood meta-theory \cite{Altenkirch2010}.

38How can we achieve both of these goals?

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

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

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

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

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

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

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

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

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

46straightforward manner, without compromising the simplicity of the underlying

47type theory.

49\subsection{Contributions}

51−A dependently typed programming language relies on several components, many of

51+A dependently-typed programming language relies on several components, many of

52which are now well understood. For example, we rely on a type checker for

53the core type theory \cite{Chapman2005epigram,loh2010tutorial}, a

54unification algorithm \cite{Miller1992} and an evaluator. However, it is less

55well understood how to combine these components effectively into a practical

56programming language.

58−The primary contribution of this paper is a tactic based method for translating

58+The primary contribution of this paper is a tactic-based method for translating

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

59+programs 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

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

@@ -66,7 +66,7 @@ description of the typing rules. Finally, through describing the specific

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

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

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

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

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

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

72\subsection{Outline}

@@ -95,11 +95,11 @@ phases, illustrated below:

95\noindent

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

97a 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

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

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

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

102−beginning with a tactic based system for constructing

102+beginning with a tactic-based system for constructing

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

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

105Section

@@ -110,8 +110,8 @@ concludes.

110

111\subsection{Typographical conventions}

112

113−This paper presents programs in two different but related languages: a high level

113+This paper presents programs in two different but related languages: a high-level

114−language \Idris{} intended for programmers, and a low level language \TT{} to

114+language \Idris{} intended for programmers, and a low-level language \TT{} to

115which \Idris{} is elaborated. We distinguish these languages typographically as

116follows:

117

@@ -131,8 +131,8 @@ in $\MO{SmallCaps}$.

131

132\subsection{Elaboration Example}

133

134−\Idris{} is a Haskell-like pure functional programming language with dependent

134+A simple example of an \Idris{}

135−types. A simple example program is the following, which adds corresponding

135+program is the following, which adds corresponding

136elements of vectors of the same length:

137

138\begin{SaveVerbatim}{vadd}

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

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

149

150\begin{itemize}

151−\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.

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

153are implicitly bound.

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

@@ -156,8 +156,8 @@ and have the same element type (\texttt{a}), and that the element type and lengt

156are preserved in the output vector.

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

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

159+\item Unlike Haskell, a single colon is used for type signatures, and a double

160−cons operator, emphasising the importance of types.

160+colon for the cons operator, emphasising the importance of types.

161\end{itemize}

162

163\noindent

papers/impl-paper/typechecking.tex+15−14

@@ -2,9 +2,9 @@

3\label{sect:typechecking}

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

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

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

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

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

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

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

10The

@@ -28,7 +28,7 @@ type of types, and may be extended with other primitives.

29The function space $\all{\vx}{\vS}\SC\vT$ may also be written as $(\vx\Hab\vS)\to\vT$,

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

31−the high level language. Universe levels on types ($\Type_i$) may be left implicit and

31+the high-level language. Universe levels on types ($\Type_i$) may be left implicit and

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

34\FFIG{

@@ -133,7 +133,7 @@ contractions and reversed contractions. Terms which are convertible are also sai

133be definitionally equal.

134The evaluator can also be extended by defining pattern matching functions, which

135will be described in more detail in Section \ref{sect:patdefs}. In principle, pattern

136−matching functions can be understood as extending the core language with high level

136+matching functions can be understood as extending the core language with high-level

137reduction rules.

138

139\FFIG{

@@ -301,10 +301,11 @@ recursive arguments have types of the form

301where $\TC{T}$ does not occur in any of the $\tS$ or the $\ty$

302This restriction is known as

303\demph{strict positivity} and ensures that recursive arguments of the

304−constructor are structurally smaller than the value itself\footnote{In

304+constructor are structurally smaller than the value itself.

305+In

305practice, this restriction can be relaxed when defining a family, but definitions

306practice, this restriction can be relaxed when defining a family, but definitions

306using families which do not satisfy strict positivity will not pass totality

307using families which do not satisfy strict positivity will not pass totality

307−checking.}.

308+checking.

308

309

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

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

310

311

@@ -611,12 +612,12 @@ is a deliberate choice --- it is a combination of small, well-understood compone

611The kernel of the \TT{} implementation, consisting of a type checker, evaluator and

612The kernel of the \TT{} implementation, consisting of a type checker, evaluator and

612pattern match compiler, is less than 1000 lines of Haskell code. If we are confident

613pattern match compiler, is less than 1000 lines of Haskell code. If we are confident

613in the correctness of the kernel of \TT{}, and any higher level language feature

614in the correctness of the kernel of \TT{}, and any higher level language feature

614−can be translated into \TT{}, we can be more confident of the correctness of the high

615+can be translated into \TT{}, we can be more confident of the correctness of

615−level language implementation than if it were implemented directly.

616+the high-level language implementation than if it were implemented directly.

616

617

617−The process of elaborating a high level language into a core type theory like \TT{} is,

618+The process of elaborating a high-level language into a core type theory like \TT{} is,

618however, less well understood, and presents several challenges depending on the

619however, less well understood, and presents several challenges depending on the

619−features of the high level language.

620+features of the high-level language.

620%Elaboration has been implemented in various different ways,

621%Elaboration has been implemented in various different ways,

621%for example in Agda~\cite{norell2007thesis} and Epigram~\cite{McBride2004a}.

622%for example in Agda~\cite{norell2007thesis} and Epigram~\cite{McBride2004a}.

622

623

@@ -688,9 +689,9 @@ syntax:

688

689

689\subsubsection{An Observation: Programming vs Theorem Proving}

690\subsubsection{An Observation: Programming vs Theorem Proving}

690

691

691−\Idris{} programs may contain several high level constructs not present in \TT{}, such

692+\Idris{} programs may contain several high-level constructs not present in \TT{}, such

692as implicit arguments, type classes, \texttt{where} clauses, pattern matching \texttt{let}

693as implicit arguments, type classes, \texttt{where} clauses, pattern matching \texttt{let}

693−and \texttt{case} constructs. We would like the high level language to be as expressive

694+and \texttt{case} constructs. We would like the high-level language to be as expressive

694as possible, while remaining possible to translate to \TT{}.

695as possible, while remaining possible to translate to \TT{}.

695

696

696Before considering how to achieve this, we make an observation about the distinction between

697Before considering how to achieve this, we make an observation about the distinction between

@@ -706,12 +707,12 @@ prover~\cite{Bertot2004}, are a convenient abstraction for building proofs and

706programs by \remph{refinement}.

707programs by \remph{refinement}.

707\end{itemize}

708\end{itemize}

708

709

709−The idea behind the \Idris{} elaborator, therefore, is to use the high level

710+The idea behind the \Idris{} elaborator, therefore, is to use the high-level

710program to direct \demph{tactics} to build \TT{} programs by refinement. The

711program to direct \demph{tactics} to build \TT{} programs by refinement. The

711elaborator is implemented as a Haskell monad capturing proof state, with a

712elaborator is implemented as a Haskell monad capturing proof state, with a

712collection of tactics for updating and refining the proof state. The remainder

713collection of tactics for updating and refining the proof state. The remainder

713of this paper describes this elaborator and demonstrates how it is used to

714of this paper describes this elaborator and demonstrates how it is used to

714−implement the high level features of \Idris{}.

715+implement the high-level features of \Idris{}.

715

716

717

718