93c06b5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Some formatting

commit93c06b5280488b1b3327322691d71fcf734ff626 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 6 Jan 2012, 15:20 (15 years ago) parent02701e7

5 files changed+23−1

compare with master

unifiedsplit

tutorial/classes.tex+3 tutorial/interp.tex+6 tutorial/provisional.tex+3−1 tutorial/theorems.tex+1 tutorial/typesfuns.tex+10

tutorial/classes.tex+3

@@ -54,6 +54,7 @@ Idris> show (S (S (S O)))

5454\end{SaveVerbatim}

5555\useverb{shownat}

5656

57+\noindent

5758Instance declarations can themselves have constraints. For example, to define a

5859\texttt{Show} instance for vectors, we need to know that there is a \texttt{Show}

5960instance for the element type, because we are going to use it to convert each element

@@ -159,6 +160,7 @@ class Eq a => Ord a where {

159160\end{SaveVerbatim}

160161\useverb{eqord}

161162

163+\noindent

162164The \texttt{Ord} class allows us to compare two values and determine their ordering.

163165Only the \texttt{compare} method is required; every other method has a default definition.

164166Using

@@ -204,6 +206,7 @@ class Monad (m : Set -> Set) where {

204206\end{SaveVerbatim}

205207\useverb{monad}

206208

209+\noindent

207210The \texttt{Monad} class allows us to encapsulate binding and computation, and is the

208211basis of \texttt{do}-notation introduced in Section \ref{sect:do}. Inside a

209212\texttt{do} block, the following syntactic transformations are applied:

tutorial/interp.tex+6

@@ -28,6 +28,7 @@ interpTy (TyFun A T) = interpTy A -> interpTy T;

2828\end{SaveVerbatim}

2929\useverb{interpty}

3030

31+\noindent

3132We're going to define a representation of our language in such a way that only

3233well-typed programs can be represented. We'll index the representations of

3334expressions by their type and the types of local variables (the context), which

@@ -75,6 +76,7 @@ data Expr : Vect Ty n -> Ty -> Set where

7576\end{SaveVerbatim}

7677\codefig{exprty}{Expression representation}

7778

79+\noindent

7880We use a nameless representation for variables --- they are \emph{de Bruijn indexed}.

7981Variables are represented by a proof of their membership in the context,

8082\texttt{HasType i G T}, which is a proof that variable \texttt{i} in context

@@ -89,6 +91,7 @@ data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where

8991\end{SaveVerbatim}

9092\useverb{hastype}

9193

94+\noindent

9295We can treat \remph{stop} as a proof that the most recently defined variable is well-typed,

9396and \remph{pop n} as a proof that, if the \texttt{n}th most recently defined variable is

9497well-typed, so is the \texttt{n+1}th. In practice, this means we use \texttt{pop} to

@@ -102,6 +105,7 @@ Var : HasType i G t -> Expr G t

102105\end{SaveVerbatim}

103106\useverb{varcon}

104107

108+\noindent

105109So, in an expression \texttt{$\backslash$x. $\backslash$y. x y},

106110the variable \texttt{x} would have a de Bruijn index

107111of 1, represented as \texttt{pop stop}, and \texttt{y 0}, represented

@@ -231,6 +235,7 @@ interp env (Val x) = x;

231235\end{SaveVerbatim}

232236\useverb{valinterp}

233237

238+\noindent

234239Lambdas are more interesting. In this case, we construct a function which

235240interprets the scope of the lambda with a new value in the environment. So, a

236241function in the object language is translated to an \Idris{} function:

@@ -242,6 +247,7 @@ interp env (Lam sc) = \x => interp (x :: env) sc;

242247\end{SaveVerbatim}

243248\useverb{laminterp}

244249

250+\noindent

245251For an application, we interpret the function and its argument and apply it

246252directly. We know that interpreting \texttt{f} must produce a function, because of its

247253type:

tutorial/provisional.tex+3−1

@@ -33,7 +33,7 @@ parity (S (S k)) with parity k {

3333\useverb{parfail}

3434

3535\noindent

36−this simply states that zero is even, one is odd, and recursively, the parity

36+This simply states that zero is even, one is odd, and recursively, the parity

3737of \texttt{k+2} is the same as the parity of \texttt{k}.

3838Explicitly marking the value of \texttt{n} in

3939even and odd is necessary to help type inference. Unfortunately, the type

@@ -88,6 +88,7 @@ parity (S (S k)) with parity k {

8888\end{SaveVerbatim}

8989\useverb{paritypro}

9090

91+\noindent

9192When written in this form, instead of reporting a type error, \Idris{} will insert

9293a metavariable standing for a theorem which will correct the type error. \Idris{}

9394tells us we have two proof obligations, with names generated from the module and

@@ -225,6 +226,7 @@ data Binary : Nat -> Set where

225226\end{SaveVerbatim}

226227\useverb{bindef}

227228

229+\noindent

228230\texttt{bO} and \texttt{bI} take a binary number as an argument and effectively shift it one bit

229231left, adding either a zero or one as the new least significant bit. The index,

230232\texttt{n + n} or \texttt{S (n + n)} states the result that this left shift then add will

tutorial/theorems.tex+1

@@ -97,6 +97,7 @@ plusReducesS (S k) m = eqRespS (plusReducesS k m);

9797\end{SaveVerbatim}

9898\useverb{plusRedS}

9999

100+\noindent

100101Even for trival theorems like these, the proofs are a little tricky to

101102construct in one go. When things get even slightly more complicated, it becomes

102103too much to think about to construct proofs in this 'batch mode'. \Idris{}

tutorial/typesfuns.tex+10

@@ -575,6 +575,7 @@ data Vect : Set -> Nat -> Set where

575575\end{SaveVerbatim}

576576\useverb{listvec}

577577

578+\noindent

578579Note that the constructor names are the same for each --- constructor names (in

579580fact, names in general) can be overloaded, provided that they are declared in

580581different namespaces (see Section \ref{sect:namespaces}), and will typically be

@@ -586,6 +587,7 @@ names \texttt{Nil} and \texttt{::} can be written in list form. For example:

586587\item \texttt{[1,2,3]} means \texttt{Cons 1 (Cons 2 (Cons 3 Nil))}

587588\end{itemize}

588589

590+\noindent

589591The library also defines a number of functions for manipulating these types.

590592\texttt{map} is overloaded both for \texttt{List} and \texttt{Vect}

591593and applies a function to every element of the list or vector.

@@ -628,6 +630,7 @@ You'll find these examples in \texttt{usefultypes.idr} in the \texttt{examples/}

628630\end{SaveVerbatim}

629631\useverb{rundvect}

630632

633+\noindent

631634For more details of the functions available on \texttt{List} and \texttt{Vect},

632635look in the library, in \texttt{prelude/list.idr} and \texttt{prelude/vect.idr} respectively.

633636Functions include filtering, appending, reversing, and so on. Also remember

@@ -681,6 +684,7 @@ data Maybe a = Just a | Nothing;

681684\end{SaveVerbatim}

682685\useverb{maybe}

683686

687+\noindent

684688\texttt{Maybe} is one way of giving a type to an operation that may fail. For example,

685689looking something up in a \texttt{List} (rather than a vector) may result in an out of

686690bounds error:

@@ -695,6 +699,7 @@ list_lookup (S k) (x :: xs) = list_lookup k xs;

695699\end{SaveVerbatim}

696700\useverb{lookuplist}

697701

702+\noindent

698703The \texttt{maybe} function is used to process values of type \texttt{Maybe},

699704either by applying a function to the value, if there is one, or by providing a default value:

700705

@@ -705,6 +710,7 @@ maybe : Maybe a -> |(default:b) -> (a -> b) -> b;

705710\end{SaveVerbatim}

706711\useverb{maybefn}

707712

713+\noindent

708714The vertical bar $\mid$ before the default value is a laziness annotation. Normally

709715expressions are evaluated before being passed to a function. This is typically

710716the most efficient behaviour. However, in this case, the default value might

@@ -723,6 +729,7 @@ data Pair a b = MkPair a b;

723729\end{SaveVerbatim}

724730\useverb{mkpair}

725731

732+\noindent

726733As syntactic sugar, we can write \texttt{(a, b)} which, according to context,

727734means either \texttt{Pair a b} or \texttt{MkPair a b}.

728735Tuples can contain an arbitrary number of values, represented as nested pairs:

@@ -751,6 +758,7 @@ data Exists : (A : Set) -> (P : A -> Set) -> Set where

751758\end{SaveVerbatim}

752759\useverb{sigma}

753760

761+\noindent

754762Again, there is syntactic sugar for this. \texttt{(a : A ** P)} is the type of a pair of

755763A and P, where the name \texttt{a} can occur inside P. \texttt{( a ** p (}

756764constructs a value of this type. For example, we can pair a number with a

@@ -790,6 +798,7 @@ vec = (_ ** [3, 4]);

790798\end{SaveVerbatim}

791799\useverb{dvec2}

792800

801+\noindent

793802One use for dependent pairs is to return values of dependent types where the

794803index is not necessarily known in advance. For example, if we filter elements

795804out of a \texttt{Vect} according to some predicate, we will not know in advance what the

@@ -812,6 +821,7 @@ vfilter p VNil = (_ , []);

812821\end{SaveVerbatim}

813822\useverb{vfilternil}

814823

824+\noindent

815825In the \texttt{::} case, we need to inspect the result of a recursive call to

816826\texttt{filter} to

817827extract the length and the vector from the result. To do this, we use \texttt{with}