d737d67 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Small library tweaks and documentation update

d737d67Edwin Brady14 years ago

lib/Prelude.idr+1−2

compare with master

unifiedsplit

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

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

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

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

56 show' acc [] = acc

55 show' acc [] = acc

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

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

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

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

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

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

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

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

62− show' : Vect a m -> String

61+ show' : Vect a n -> String

63 show' [] = ""

62 show' [] = ""

64 show' [x] = show x

63 show' [x] = show x

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

64 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

166further than the outer function.

167

168\textbf{Remark (scope):}

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

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

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

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

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

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

172−in scope. In particular,

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

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

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

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

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

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

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

176−

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

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}

186

177

187\subsubsection{Dependent Types}

178\subsubsection{Dependent Types}

188

179

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

210declaration: it explicitly states the type

201declaration: it explicitly states the type

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

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

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

203argument, 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

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.

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

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

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

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

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

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

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

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

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

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

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

425

418

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

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

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

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

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

421+ show' : Vect a n -> String

429 show' Nil = ""

422 show' Nil = ""

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

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

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

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

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

433\end{SaveVerbatim}

426\end{SaveVerbatim}

434\useverb{showvec}

427\useverb{showvec}

435

428

436−\noindent

429+%\noindent

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

430+%\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

431+%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

432+%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

433+%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

434+%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,

435+%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'}.

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

444

437

438+\noindent

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

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

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

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

447\texttt{Eq} class:

441\texttt{Eq} class:

tutorial/classes.tex+9−9

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

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

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

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

66+ show' : Vect a n -> String

67 show' Nil = ""

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

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

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

71\end{SaveVerbatim}

72\useverb{showvec}

74−\noindent

74+%\noindent

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

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

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

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}

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

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,

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'}.

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

83\subsection{Default Definitions}

tutorial/typesfuns.tex+5−17

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

210further than the outer function.

211

212\textbf{Scope:}

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

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

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

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

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

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

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

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

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

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

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

219

218

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

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

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

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

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

233the definition of \texttt{foo}:

221the definition of \texttt{foo}: