@@ -42,7 +42,9 @@ inferred by the machine~\cite{pollack1990implicit}.
4242 \mid & \vb\SC\;\vt & (\mbox{binding}) &
4343 \mid & \all{\vx}{\vt} & (\mbox{function space}) \\
4444
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}) &
4648% \mid & \pat{\vx}{\vt} & (\mbox{pattern variable}) \\
4749% & & &
4850% \mid & \pty{\vx}{\vt} & (\mbox{pattern type}) \\
@@ -83,6 +85,11 @@ $\LET$ binding:
8385{\Gamma;\LET\;\vx\;\defq\;\vs\Hab\vS\proves\RW{valid}}
8486}
8587
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+
8693\subsubsection{Evaluation}
8794
8895\label{sect:evaluation}
@@ -153,7 +160,10 @@ lower universe levels to inhabit higher universe levels. In practice, universe l
153160can be left implicit (and will be left implicit in the rest of this paper) ---
154161the type checker generates a graph of constraints between universe levels (such
155162as that produced by the $\mathsf{Forall}$ typing rule) and checks that there
156−are no cycles. Otherwise, the typing rules are standard and type inference can
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.
166+Otherwise, the typing rules are standard and type inference can
157167be implemented in the usual way~\cite{loh2010tutorial}.
158168
159169\FFIG{\begin{array}{c}
@@ -263,15 +273,26 @@ sequence of zero or more $\vx$ (i.e., $\vx_1,\vx_2,\ldots,\vx_n$):
263273\DM{
264274\AR{
265275\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+}
267278}
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
268287}
269288
270−Constructors may take recursive arguments in the family $\TC{T}$, which may be
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
289+where $\TC{T}$ does not occur in any of the $\tS$ or the $\ty$
290+This restriction is known as
273291\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.}.
275296
276297For example, the \Idris{} data type \tTC{Nat} would be declared in \TT{} as follows:
277298
@@ -542,7 +563,9 @@ are marked as \emph{partial}. Additionally, any function which calls a partial
542563function or uses a data type which is not strictly positive is also marked as
543564partial. We use the size change principle~\cite{Lee2001} to determine whether
544565(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.
546569\TT{} also marks functions which do not cover
547570all possible inputs as partial. This totality checking is independent of the
548571rest of the type theory, and can be extended.