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

git.iko.soy/Idris-dev

on master help sign in

Some formatting

93c06b5Edwin Brady15 years ago

tutorial/classes.tex+3

compare with master

unifiedsplit

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

54\end{SaveVerbatim}

55\useverb{shownat}

57+\noindent

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

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

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

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

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

60instance 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 {

159\end{SaveVerbatim}

160\end{SaveVerbatim}

160\useverb{eqord}

161\useverb{eqord}

161

162

163+\noindent

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

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

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

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

164Using

166Using

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

204\end{SaveVerbatim}

206\end{SaveVerbatim}

205\useverb{monad}

207\useverb{monad}

206

208

209+\noindent

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

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

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

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

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

212\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;

28\end{SaveVerbatim}

29\useverb{interpty}

31+\noindent

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

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

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

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

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

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

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

75\end{SaveVerbatim}

76\end{SaveVerbatim}

76\codefig{exprty}{Expression representation}

77\codefig{exprty}{Expression representation}

79+\noindent

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

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

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

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

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

82\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

89\end{SaveVerbatim}

91\end{SaveVerbatim}

90\useverb{hastype}

92\useverb{hastype}

94+\noindent

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

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

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

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

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

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

102\end{SaveVerbatim}

105\end{SaveVerbatim}

103\useverb{varcon}

106\useverb{varcon}

104

107

108+\noindent

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

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

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

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

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

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

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

231\end{SaveVerbatim}

235\end{SaveVerbatim}

232\useverb{valinterp}

236\useverb{valinterp}

233

237

238+\noindent

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

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

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

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

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

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

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

242\end{SaveVerbatim}

247\end{SaveVerbatim}

243\useverb{laminterp}

248\useverb{laminterp}

244

249

250+\noindent

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

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

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

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

247type:

253type:

tutorial/provisional.tex+3−1

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

33\useverb{parfail}

35\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

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

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

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

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

88\end{SaveVerbatim}

89\useverb{paritypro}

91+\noindent

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

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

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

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

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

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

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

225\end{SaveVerbatim}

226\end{SaveVerbatim}

226\useverb{bindef}

227\useverb{bindef}

227

228

229+\noindent

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

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

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

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

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

232\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);

97\end{SaveVerbatim}

98\useverb{plusRedS}

100+\noindent

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

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

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

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

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

103too 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

575\end{SaveVerbatim}

576\useverb{listvec}

577

578+\noindent

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

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

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

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

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

581different 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:

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

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

587\end{itemize}

588\end{itemize}

588

589

590+\noindent

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

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

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

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

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

593and 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/}

628\end{SaveVerbatim}

630\end{SaveVerbatim}

629\useverb{rundvect}

631\useverb{rundvect}

630

632

633+\noindent

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

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

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

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

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

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

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

681\end{SaveVerbatim}

684\end{SaveVerbatim}

682\useverb{maybe}

685\useverb{maybe}

683

686

687+\noindent

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

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

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

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

686bounds error:

690bounds error:

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

695\end{SaveVerbatim}

699\end{SaveVerbatim}

696\useverb{lookuplist}

700\useverb{lookuplist}

697

701

702+\noindent

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

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

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

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

700

705

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

705\end{SaveVerbatim}

710\end{SaveVerbatim}

706\useverb{maybefn}

711\useverb{maybefn}

707

712

713+\noindent

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

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

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

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

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

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

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

723\end{SaveVerbatim}

729\end{SaveVerbatim}

724\useverb{mkpair}

730\useverb{mkpair}

725

731

732+\noindent

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

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

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

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

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

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

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

751\end{SaveVerbatim}

758\end{SaveVerbatim}

752\useverb{sigma}

759\useverb{sigma}

753

760

761+\noindent

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

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

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

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

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

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

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

790\end{SaveVerbatim}

798\end{SaveVerbatim}

791\useverb{dvec2}

799\useverb{dvec2}

792

800

801+\noindent

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

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

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

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

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

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

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

812\end{SaveVerbatim}

821\end{SaveVerbatim}

813\useverb{vfilternil}

822\useverb{vfilternil}

814

823

824+\noindent

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

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

816\texttt{filter} to

826\texttt{filter} to

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

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