db1e94f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Some implementation paper adjustments

db1e94fEdwin Brady13 years ago

papers/impl-paper/elaboration.tex+2

compare with master

unifiedsplit

@@ -247,6 +247,8 @@ the hole queue. $\MO{Focus}\;\vn$ moves a hole to the head of the hole queue:

247}

248

249\noindent

250+$\MO{Focus}$ refers to a hole $\vn$ by name. Hole names are either given

251+explicitly in proofs, or chosen (as fresh names) by tactics.

250Correspondingly, $\MO{Unfocus}$ moves the currently in focus hole to the

252Correspondingly, $\MO{Unfocus}$ moves the currently in focus hole to the

251end of the hole queue:

253end of the hole queue:

252

254

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

@@ -110,7 +110,9 @@ mult (S k) y = plus y (mult k y)

110The standard arithmetic operators \texttt{+} and \texttt{*} are also overloaded

111for use by \texttt{Nat}, and are implemented

112using the above functions. Unlike Haskell, there is no restriction on whether

113−types and function names must begin with a capital letter or not.

113+types and function names must begin with a capital letter or not. Indeed, such

114+a distinction would not necessarily be helpful, since function names may

115+appear in pattern context if forced by some dependency.

114%Function

116%Function

115%names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S},

117%names (\tFN{plus} and \tFN{mult} above), data constructors (\tDC{O}, \tDC{S},

116%\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are

118%\tDC{Nil} and \tDC{::}) and type constructors (\tTC{Nat} and \tTC{List}) are

@@ -192,9 +194,9 @@ data Vect : Nat -> Type -> Type where

192Note that this uses the same constructor names as for \tTC{List}. Ad-hoc name

194Note that this uses the same constructor names as for \tTC{List}. Ad-hoc name

193overloading such as this is accepted by \Idris{}, provided that the names are

195overloading such as this is accepted by \Idris{}, provided that the names are

194declared in different namespaces (in practice, normally in different modules)

196declared in different namespaces (in practice, normally in different modules)

195−so that the names are different internally. Namespace resolution can be made

197+so that the names are different internally. Names can be used qualified by

196−explicitly (e.g. \texttt{List.Nil} or \texttt{Vect.Nil}) or more commonly

198+a namespace (e.g. \texttt{Vect.Nil}) or unqualified. If unqualified, it must

197−by type.

199+be possible to distinguish between names by type.

198

200

199The above declaration creates a family of types, and requires a different form

201The above declaration creates a family of types, and requires a different form

200of declaration from the simple type declarations above. It resembles a Haskell

202of declaration from the simple type declarations above. It resembles a Haskell

@@ -642,6 +644,8 @@ intermediate computation (\texttt{even} and \texttt{odd}) right of the

642the results affect the other patterns left of the $\mid$. Note that there is a

644the results affect the other patterns left of the $\mid$. Note that there is a

643function in the patterns (\texttt{+}) and repeated occurrences of \texttt{j} ---

645function in the patterns (\texttt{+}) and repeated occurrences of \texttt{j} ---

644this is allowed

646this is allowed

645−because another argument has determined the form of these patterns.

647+because another argument has determined the form of these patterns. In general,

648+non-linear patterns are allowed \emph{only} when their value is forced by

649+some other argument.

646

650

647

651

papers/impl-paper/typechecking.tex+31−8

@@ -42,7 +42,9 @@ inferred by the machine~\cite{pollack1990implicit}.

42 \mid & \vb\SC\;\vt & (\mbox{binding}) &

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

45− \mid & \vt\;\vt & (\mbox{application}) &

45+ \mid & \vt\;\vt & (\mbox{application}) & \\

46+ \mid & \TC{T} & (\mbox{type constructor}) & \\

47+ \mid & \TC{D} & (\mbox{data constructor}) &

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

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

47% & & &

49% & & &

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

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

@@ -83,6 +85,11 @@ $\LET$ binding:

83{\Gamma;\LET\;\vx\;\defq\;\vs\Hab\vS\proves\RW{valid}}

85{\Gamma;\LET\;\vx\;\defq\;\vs\Hab\vS\proves\RW{valid}}

84}

86}

88+\noindent

89+We record the binding form in the context, as well as the type,

90+because type checking relies on evaluation. In particular, $\LET$ bound

91+names may reduce.

92+

86\subsubsection{Evaluation}

93\subsubsection{Evaluation}

88\label{sect:evaluation}

95\label{sect:evaluation}

@@ -153,7 +160,10 @@ lower universe levels to inhabit higher universe levels. In practice, universe l

153can be left implicit (and will be left implicit in the rest of this paper) ---

160can be left implicit (and will be left implicit in the rest of this paper) ---

154the type checker generates a graph of constraints between universe levels (such

161the type checker generates a graph of constraints between universe levels (such

155as that produced by the $\mathsf{Forall}$ typing rule) and checks that there

162as that produced by the $\mathsf{Forall}$ typing rule) and checks that there

163+are no cycles. This happens as the last stage of type checking, waiting until

164+we have all uses of a family to establish how many levels are needed in the

165+universe hierarchy.

156−are no cycles. Otherwise, the typing rules are standard and type inference can

166+Otherwise, the typing rules are standard and type inference can

157be implemented in the usual way~\cite{loh2010tutorial}.

167be implemented in the usual way~\cite{loh2010tutorial}.

158

168

159\FFIG{\begin{array}{c}

169\FFIG{\begin{array}{c}

@@ -263,15 +273,26 @@ sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$):

263\DM{

273\DM{

264\AR{

274\AR{

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

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

266−\DC{c}_1\Hab\vt\;\mid\;\ldots\;\mid\;\DC{c}_n\Hab\vt

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

277+}

267}

278}

279+

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

281+$\TC{T}$.

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

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

284+

285+\DM{

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

268}

287}

269

288

270−Constructors may take recursive arguments in the family $\TC{T}$, which may be

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

271−higher order. Higher order recursive arguments may be computed from any type

272−which does not involve $\TC{T}$ itself. This restriction is known as

290+This restriction is known as

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

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

274−constructor are structurally smaller than the value itself.

292+constructor are structurally smaller than the value itself\footnote{In

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

294+using families which do not satisfy strict positivity will not pass totality

295+checking.}.

275

296

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

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

277

298

@@ -542,7 +563,9 @@ are marked as \emph{partial}. Additionally, any function which calls a partial

542function or uses a data type which is not strictly positive is also marked as

563function or uses a data type which is not strictly positive is also marked as

543partial. We use the size change principle~\cite{Lee2001} to determine whether

564partial. We use the size change principle~\cite{Lee2001} to determine whether

544(possibly mutually defined) recursive functions are guaranteed to

565(possibly mutually defined) recursive functions are guaranteed to

545−terminate.

566+terminate. Higher order function arguments are assumed to be total, though

567+if a higher order function is called with a partial function as an argument,

568+the calling function will be marked partial.

546\TT{} also marks functions which do not cover

569\TT{} also marks functions which do not cover

547all possible inputs as partial. This totality checking is independent of the

570all possible inputs as partial. This totality checking is independent of the

548rest of the type theory, and can be extended.

571rest of the type theory, and can be extended.