d737d67 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Small library tweaks and documentation update

commitd737d670d1d33c6bbcf1eb981e1738434b2a4898 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 7 Feb 2013, 17:56 (14 years ago) parenta76f8b3

4 files changed+38−57

compare with master

unifiedsplit

lib/Prelude.idr+1−2 papers/impl-paper/hll.tex+23−29 tutorial/classes.tex+9−9 tutorial/typesfuns.tex+5−17

lib/Prelude.idr+1−2

@@ -52,14 +52,13 @@ instance (Show a, Show b) => Show (a, b) where

5252

5353instance Show a => Show (List a) where

5454 show xs = "[" ++ show' "" xs ++ "]" where

55− show' : String -> List a -> String

5655 show' acc [] = acc

5756 show' acc [x] = acc ++ show x

5857 show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs

5958

6059instance Show a => Show (Vect a n) where

6160 show xs = "[" ++ show' xs ++ "]" where

62− show' : Vect a m -> String

61+ show' : Vect a n -> String

6362 show' [] = ""

6463 show' [x] = show x

6564 show' (x :: xs) = show x ++ ", " ++ show' xs

papers/impl-paper/hll.tex+23−29

@@ -166,23 +166,14 @@ Indentation is significant --- functions in the \texttt{where} block must be ind

166166further than the outer function.

167167

168168\textbf{Remark (scope):}

169−Any names which are visible in the outer scope are also visible in the \texttt{where}

170−clause (unless they have been redefined, such as \texttt{xs} here).

171−\emph{However}, names which appear in the type are \emph{not} automatically

172−in scope. In particular,

173−in the above example, the \texttt{a} in the top level type and the \texttt{a} in the

174−auxiliary definition \texttt{revAcc} are \emph{not} the same. If this is the required

175−behaviour, the \texttt{a} can be brought into scope as follows:

176−

177−\begin{SaveVerbatim}{revwhereb}

178−

179−reverse : List a -> List a

180−reverse {a} xs = revAcc [] xs where

181− revAcc : List a -> List a -> List a

182− ...

183−

184−\end{SaveVerbatim}

185−\useverb{revwhereb}

169+Any names which are visible in the outer scope are also visible in the

170+\texttt{where} clause (unless they are redefined in the \texttt{where} clause,

171+such as \texttt{xs} here). A name which appears only in the type will be in

172+scope in the \texttt{where} clause if it is a \remph{parameter} to one of the

173+types, i.e. it is fixed across the entire structure. In particular, this means

174+that the \texttt{a} in the definition of \texttt{reverse} above is the

175+\remph{same} \texttt{a} as in the definition of \texttt{revAcc}, as \texttt{a}

176+is a parameter of \texttt{List}.

186177

187178\subsubsection{Dependent Types}

188179

@@ -210,9 +201,11 @@ from the simple type declarations above. It resembles a Haskell GADT

210201declaration: it explicitly states the type

211202of the type constructor \tTC{Vect} --- it takes a type and a \tTC{Nat} as an

212203argument, where \tTC{Type} stands for the type of types. We say that \tTC{Vect}

213−is \emph{parameterised} by a type, and \emph{indexed} over \tTC{Nat}. Each

214−constructor targets a different part of the family of types. \tDC{Nil} can only

215−be used to construct vectors with zero length, and \tDC{::} to construct

204+is \emph{parameterised} by a type, and \emph{indexed} over \tTC{Nat}.

205+The distinction between parameters and indices is that a parameter is fixed

206+across an entire structure, whereas an index may vary.

207+Each constructor targets a different part of the family of types. \tDC{Nil} can

208+only be used to construct vectors with zero length, and \tDC{::} to construct

216209vectors with non-zero length. The type of \tDC{::} states explicitly that an element

217210of type \texttt{a} and a tail of type \texttt{Vect a k} (i.e., a vector of length \texttt{k})

218211combine to make a vector of length \texttt{S k}.

@@ -425,7 +418,7 @@ to a \texttt{String}:

425418

426419instance Show a => Show (Vect a n) where

427420 show xs = "[" ++ show' xs ++ "]" where

428− show' : Vect a n' -> String

421+ show' : Vect a n -> String

429422 show' Nil = ""

430423 show' (x :: Nil) = show x

431424 show' (x :: xs) = show x ++ ", " ++ show' xs

@@ -433,15 +426,16 @@ instance Show a => Show (Vect a n) where

433426\end{SaveVerbatim}

434427\useverb{showvec}

435428

436−\noindent

437−\textbf{Remark: } The type of the auxiliary function \texttt{show'} is

438−important. The type variables \texttt{a} and \texttt{n} which are part of the

439−instance declaration for \texttt{Show (Vect a n)} are fixed across the entire

440−instance declaration. As a result, \texttt{a} need not be constrained

441−again. Furthermore, it means that if \texttt{n} is used again in the type, it refers

442−to the (fixed) length of the outermost list \texttt{xs}. Therefore,

443−there is a different name for the length \texttt{n'} in \texttt{show'}.

429+%\noindent

430+%\textbf{Remark: } The type of the auxiliary function \texttt{show'} is

431+%important. The type variables \texttt{a} and \texttt{n} which are part of the

432+%instance declaration for \texttt{Show (Vect a n)} are fixed across the entire

433+%instance declaration. As a result, \texttt{a} need not be constrained

434+%again. Furthermore, it means that if \texttt{n} is used again in the type, it refers

435+%to the (fixed) length of the outermost list \texttt{xs}. Therefore,

436+%there is a different name for the length \texttt{n'} in \texttt{show'}.

444437

438+\noindent

445439Like Haskell type classes, default definitions can be given in the class declaration.

446440Otherwise, all methods must be given in an instance. For example, there is an

447441\texttt{Eq} class:

tutorial/classes.tex+9−9

@@ -63,7 +63,7 @@ to a \texttt{String}:

6363

6464instance Show a => Show (Vect a n) where

6565 show xs = "[" ++ show' xs ++ "]" where

66− show' : Vect a n' -> String

66+ show' : Vect a n -> String

6767 show' Nil = ""

6868 show' (x :: Nil) = show x

6969 show' (x :: xs) = show x ++ ", " ++ show' xs

@@ -71,14 +71,14 @@ instance Show a => Show (Vect a n) where

7171\end{SaveVerbatim}

7272\useverb{showvec}

7373

74−\noindent

75−\textbf{Remark: } The type of the auxiliary function \texttt{show'} is

76−important. The type variables \texttt{a} and \texttt{n} which are part of the

77−instance declaration for \texttt{Show (Vect a n)} are fixed across the entire

78−instance declaration. As a result, we do not have to constrain \texttt{a}

79−again. Furthermore, it means that if we use \texttt{n} in the type, it refers

80−to the (fixed) length of the outermost list \texttt{xs}. Therefore,

81−we use a different name for the length \texttt{n'} in \texttt{show'}.

74+%\noindent

75+%\textbf{Remark: } The type of the auxiliary function \texttt{show'} is

76+%important. The type variables \texttt{a} and \texttt{n} which are part of the

77+%instance declaration for \texttt{Show (Vect a n)} are fixed across the entire

78+%instance declaration. As a result, we do not have to constrain \texttt{a}

79+%again. Furthermore, it means that if we use \texttt{n} in the type, it refers

80+%to the (fixed) length of the outermost list \texttt{xs}. Therefore,

81+%we use a different name for the length \texttt{n'} in \texttt{show'}.

8282

8383\subsection{Default Definitions}

8484

tutorial/typesfuns.tex+5−17

@@ -210,24 +210,12 @@ Indentation is significant --- functions in the \texttt{where} block must be ind

210210further than the outer function.

211211

212212\textbf{Scope:}

213−Any names which are visible in the outer scope are also visible in the \texttt{where}

214−clause (unless they have been redefined, such as \texttt{xs} here).

215−\emph{However}, names which appear in the type are \emph{not} in scope. In particular,

216−in the above example, the \texttt{a} in the top level type and the \texttt{a} in the

217−auxiliary definifion \texttt{revAcc} are \emph{not} the same. If this is the required

218−behaviour, the \texttt{a} can be brought into scope as follows:

213+Any names which are visible in the outer scope are also visible in the

214+\texttt{where} clause (unless they have been redefined, such as \texttt{xs}

215+here). A name which appears only in the type will be in scope in the

216+\texttt{where} clause if it is a \remph{parameter} to one of the types,

217+i.e. it is fixed across the entire structure.

219218

220−\begin{SaveVerbatim}{revwhereb}

221−

222−reverse : List a -> List a

223−reverse {a} xs = revAcc [] xs where

224− revAcc : List a -> List a -> List a

225− ...

226−

227−\end{SaveVerbatim}

228−\useverb{revwhereb}

229−

230−\noindent

231219As well as functions, \texttt{where} blocks can include local data

232220declarations, such as the following where \texttt{MyLT} is not accessible outside

233221the definition of \texttt{foo}: