1862197 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Switch Vect arguments in implementation paper

1862197Edwin Brady13 years ago

papers/impl-paper/elaboration.tex+11−11

compare with master

unifiedsplit

@@ -457,10 +457,10 @@ For example, consider the following proof term:

457

458\DM{

459\AR{

460−\hole{\vA}{\Type}\SC\hole{\vk}{\Nat}\SC

460+\hole{\va}{\Type}\SC\hole{\vk}{\Nat}\SC

461−\hole{\vx}{\vA}\SC\hole{\vxs}{\Vect\;\vA\;\vk}\SC

461+\hole{\vx}{\va}\SC\hole{\vxs}{\Vect\;\vk\;\va}\SC

462\\

463−\hole{\vys}{\Vect\;\vA\;(\suc\;\vk)}\SC\vys

463+\hole{\vys}{\Vect\;(\suc\;\vk)\;\va}\SC\vys

464}

465}

466

@@ -481,9 +481,9 @@ Therefore the resulting proof term is:

481\DM{

482\AR{

483\hole{\vk}{\Nat}\SC

484−\guess{\vx}{\TC{Int}}{42}\SC\hole{\vxs}{\Vect\;\TC{Int}\;\vk}\SC

484+\guess{\vx}{\TC{Int}}{42}\SC\hole{\vxs}{\Vect\;\vk\;\TC{Int}}\SC

485\\

486−\hole{\vys}{\Vect\;\TC{Int}\;(\suc\;\vk)}\SC\vys

486+\hole{\vys}{\Vect\;(\suc\;\vk)\;\TC{Int}}\SC\vys

487}

488}

489

@@ -895,7 +895,7 @@ of \texttt{vAdd}:

895

896\begin{SaveVerbatim}{vAddImpT}

897

898−vAdd : Num a => Vect a n -> Vect a n -> Vect a n

898+vAdd : Num a => Vect n a -> Vect n a -> Vect n a

899

900\end{SaveVerbatim}

901\useverb{vAddImpT}

@@ -907,7 +907,7 @@ type declaration:

907\begin{SaveVerbatim}{vAddImpT}

908

909vAdd : (a : _) -> (n : _) -> (c : Num a) ->

910− (xs : Vect a n) -> (ys : Vect a n) -> Vect a n

910+ (xs : Vect n a) -> (ys : Vect n a) -> Vect n a

911

912\end{SaveVerbatim}

913\useverb{vAddImpT}

@@ -1016,8 +1016,8 @@ elaboration of expressions. \IdrisM{} expression syntax is given in Figure

1016\IdrisM{} is a subset of \Idris{} without syntactic sugar --- that is, without

1017\texttt{do}-notation or infix operators --- and with implicit

1018arguments in types bound explicitly

1019−(e.g. $\piimp{\va}{\_}\piimp{\vn}{\_}\TC{Vect}\;\va\;\vn$

1019+(e.g. $\piimp{\va}{\_}\piimp{\vn}{\_}\TC{Vect}\;\vn\;\va$

1020−instead of simply $\Vect\;\va\;\vn$).

1020+instead of simply $\Vect\;\vn\;\va$).

1021Note that we separate implicit and type constraint bindings, to ensure that they

1022only appear in top level declarations.

1023It is in general straightforward to

@@ -1816,7 +1816,7 @@ the vector append function, containing a metavariable \texttt{append\_rec}:

1816

1817\begin{SaveVerbatim}{vappmv}

1818

1819−(++) : Vect a n -> Vect a m -> Vect a (n + m)

1819+(++) : Vect n a -> Vect m a -> Vect (n + m) a

1820Nil ++ ys = ys

1821(x :: xs) ++ ys = x :: ?append_rec

1822

@@ -1832,7 +1832,7 @@ We can inspect the type of \texttt{append\_rec} at the \Idris{} prompt:

1832

1833*vec> :t append_rec

1834append_rec : (a : Type) -> (m : Nat) -> (n : Nat) -> a ->

1835− Vect a n -> Vect a m -> Vect a (n + m)

1835+ Vect n a -> Vect m a -> Vect (n + m) a

1836

1837\end{SaveVerbatim}

1838\useverb{appendrec}

papers/impl-paper/hll.tex+22−22

@@ -56,7 +56,7 @@ library:

57\begin{SaveVerbatim}{natlist}

59−data Nat = O | S Nat -- Natural numbers

59+data Nat = Z | S Nat -- Natural numbers

60 -- (zero and successor)

61data List a = Nil | (::) a (List a) -- Polymorphic lists

@@ -181,9 +181,9 @@ literature. In \Idris{}, vectors are declared as follows:

181

182\begin{SaveVerbatim}{vect}

183

184−data Vect : Type -> Nat -> Type where

184+data Vect : Nat -> Type -> Type where

185− Nil : Vect a O

185+ Nil : Vect Z a

186− (::) : a -> Vect a k -> Vect a (S k)

186+ (::) : a -> Vect k a -> Vect (S k) a

187

188\end{SaveVerbatim}

189\useverb{vect}

@@ -199,15 +199,15 @@ by type.

199The above declaration creates a family of types, and requires a different form

200of declaration from the simple type declarations above. It resembles a Haskell

201GADT declaration: it explicitly states the type

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

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

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

203+arguments, where \tTC{Type} stands for the type of types. We say that \tTC{Vect}

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

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

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

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

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

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

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

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

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

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

212

213Functions on dependent types such as \tTC{Vect} are declared in the same way

@@ -218,7 +218,7 @@ library, appends two \tTC{Vect}s:

218

219\begin{SaveVerbatim}{vapp}

220

221−(++) : Vect A n -> Vect A m -> Vect A (n + m)

221+(++) : Vect n a -> Vect m a -> Vect (n + m) a

222Nil ++ ys = ys

223(x :: xs) ++ ys = x :: xs ++ ys

224

@@ -233,7 +233,7 @@ They are declared as follows in the library:

233\begin{SaveVerbatim}{findecl}

234

235data Fin : Nat -> Type where

236− fO : Fin (S k)

236+ fZ : Fin (S k)

237 fS : Fin k -> Fin (S k)

238

239\end{SaveVerbatim}

@@ -241,7 +241,7 @@ data Fin : Nat -> Type where

241

242\noindent

243This declares

244−\tDC{fO} as the zeroth element of a finite set with \texttt{S k} elements;

244+\tDC{fZ} as the zeroth element of a finite set with \texttt{S k} elements;

245\texttt{fS n} as the

246\texttt{n+1}th element of a finite set with \texttt{S k} elements.

247\tTC{Fin} is indexed by \tTC{Nat}, which

@@ -259,8 +259,8 @@ by a bounded index given as a \tTC{Fin n}, is defined in the library:

259

260\begin{SaveVerbatim}{vindex}

261

262−index : Fin n -> Vect a n -> a

262+index : Fin n -> Vect n a -> a

263−index fO (x :: xs) = x

263+index fZ (x :: xs) = x

264index (fS k) (x :: xs) = index k xs

265

266\end{SaveVerbatim}

@@ -284,7 +284,7 @@ Let us take a closer look at the type of \texttt{index}:

284

285\begin{SaveVerbatim}{vindexty}

286

287−index : Fin n -> Vect a n -> a

287+index : Fin n -> Vect n a -> a

288

289\end{SaveVerbatim}

290\useverb{vindexty}

@@ -297,7 +297,7 @@ arguments to \texttt{index}. The type of \texttt{index} could also be written as

297

298\begin{SaveVerbatim}{vindeximppl}

299

300−index : {a:_} -> {n:_} -> Fin n -> Vect a n -> a

300+index : {a:_} -> {n:_} -> Fin n -> Vect n a -> a

301

302\end{SaveVerbatim}

303\useverb{vindeximppl}

@@ -308,7 +308,7 @@ their types, to be inferred by the machine. These types could also be given expl

308

309\begin{SaveVerbatim}{vindeximpty}

310

311−index : {a:Type} -> {n:Nat} -> Fin n -> Vect a n -> a

311+index : {a:Type} -> {n:Nat} -> Fin n -> Vect n a -> a

312

313\end{SaveVerbatim}

314\useverb{vindeximpty}

@@ -316,7 +316,7 @@ index : {a:Type} -> {n:Nat} -> Fin n -> Vect a n -> a

316\noindent

317Implicit arguments, given in braces \texttt{\{\}} in the type signature, are

318not given in applications of \texttt{index}; their values can be inferred from

319−the types of the \texttt{Fin n} and \texttt{Vect a n} arguments. Any name which

319+the types of the \texttt{Fin n} and \texttt{Vect n a} arguments. Any name which

320appears as a parameter or index in a type signature, but which is otherwise

321free, will be automatically bound as an implicit argument. Implicit arguments

322can still be given explicitly in applications, using the syntax

@@ -335,7 +335,7 @@ the type of \texttt{index} could be declared as:

335

336\begin{SaveVerbatim}{vindexn}

337

338−index : (i:Fin n) -> (xs:Vect a n) -> a

338+index : (i:Fin n) -> (xs:Vect n a) -> a

339

340\end{SaveVerbatim}

341\useverb{vindexn}

@@ -359,7 +359,7 @@ example, recall the \texttt{vAdd} function:

359

360\begin{SaveVerbatim}{vadd}

361

362−total vAdd : Num a => Vect a n -> Vect a n -> Vect a n

362+total vAdd : Num a => Vect n a -> Vect n a -> Vect n a

363vAdd [] [] = []

364vAdd (x :: xs) (y :: ys) = x + y :: vAdd xs ys

365

@@ -450,9 +450,9 @@ to a \texttt{String}:

450

451\begin{SaveVerbatim}{showvec}

452

453−instance Show a => Show (Vect a n) where

453+instance Show a => Show (Vect n a) where

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

455− show' : Vect a n -> String

455+ show' : Vect n a -> String

456 show' Nil = ""

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

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

@@ -570,7 +570,7 @@ determined by whether the vector was empty or not:

570

571\begin{SaveVerbatim}{appdep}

572

573−(++) : Vect a n -> Vect a m -> Vect a (n + m)

573+(++) : Vect n a -> Vect m a -> Vect (n + m) a

574(++) {n=O} [] [] = []

575(++) {n=S k} (x :: xs) ys = x :: xs ++ ys

576

papers/impl-paper/intro.tex+4−4

@@ -109,7 +109,7 @@ elements of vectors of the same length:

109

110\begin{SaveVerbatim}{vadd}

111

112−vAdd : Num a => Vect a n -> Vect a n -> Vect a n

112+vAdd : Num a => Vect n a -> Vect n -> Vect n a

113vAdd [] [] = []

114vAdd (x :: xs) (y :: ys) = x + y :: vAdd xs ys

115

@@ -143,14 +143,14 @@ The \TT{} translation of \texttt{vAdd} is:

143\DM{

144\AR{

145\FN{vAdd} \Hab(\va\Hab\Type)\to(\vn\Hab\Nat)\to\TC{Num}\;\va\to

146− \Vect\;\va\;\vn\to\Vect\;\va\;\vn\to\Vect\;\va\;\vn\\

146+ \Vect\;\vn\;\va\to\Vect\;\vn\;\va\to\Vect\;\vn\;\va\\

147\RW{var}\;\va\Hab\Type,\;\vc\Hab\TC{Num}\;\va\SC\\

148\hg\FN{vAdd} \; \va \; \Z \; \vc \; (\DC{Nil}\;\va) \; (\DC{Nil}\;\va) \;

149\cq\;\DC{Nil}\;\va \\

150\RW{var}\;\AR{

151\va\Hab\Type,\;\vk\Hab\Nat,\;\vc\Hab\TC{Num}\;\va,\\

152−\vx\Hab\va,\;\vxs\Hab\Vect\;\va\;\vk,\;

152+\vx\Hab\va,\;\vxs\Hab\Vect\;\vk\;\va,\;

153−\vy\Hab\va,\;\vys\Hab\Vect\;\va\;\vk

153+\vy\Hab\va,\;\vys\Hab\Vect\;\vk\;\va

154\SC

155\\

156\FN{vAdd} \; \va \; (\suc\;\vk) \; \vc

papers/impl-paper/library.ltx+1−1

@@ -142,7 +142,7 @@

142

143\newcommand{\NatPackage}{

144 \newcommand{\Nat}{\TC{Nat}}

145− \newcommand{\Z}{\DC{O}}

145+ \newcommand{\Z}{\DC{Z}}

146 \newcommand{\suc}{\DC{S}}

147 \newcommand{\NatDecl}{

148 \Data \hg

papers/impl-paper/typechecking.tex+9−9

@@ -285,7 +285,7 @@ example, the \TT{} equivalent of \tTC{List} is parameterised over its element ty

285

286\DM{

287\AR{

288−\Data\hg\List\:(\va\Hab\Type)\Hab\Type\hg\Where\\

288+\Data\hg\List\Hab(\va\Hab\Type)\to\Type\hg\Where\\

289\hg\hg

290\ARd{

291& \nil\Hab\List\;\va\\

@@ -304,11 +304,11 @@ index $\vk$ is given \remph{explicitly}.

304

305\DM{

306\AR{

307−\Data\hg\Vect\;(\va\Hab\Type)\Hab\Nat\to\Type\hg\Where \\

307+\Data\hg\Vect\Hab\Nat\to(\va\Hab\Type)\to\Type\hg\Where \\

308\hg\hg\ARd{

309−& \nil\Hab\Vect\;\va\;\Z\\

309+& \nil\Hab\Vect\;\Z\;\va\\

310\mid & (\cons)\Hab\fbind{\vk}{\Nat}{

311−\fbind{\vx}{\va}{\fbind{\vxs}{\Vect\;\va\;\vk}{\Vect\;\va\;(\suc\;\vk)}}

311+\fbind{\vx}{\va}{\fbind{\vxs}{\Vect\;\vk\;\va}{\Vect\;(\suc\;\vk)\;\va}}

312}

313}

314}

@@ -584,7 +584,7 @@ also treated as an implicit argument, to which we give the name \texttt{c}:

584

585\begin{SaveVerbatim}{vAddImp}

586

587−vAdd : (a : _) -> (n : _) -> Num a -> Vect a n -> Vect a n -> Vect a n

587+vAdd : (a : _) -> (n : _) -> Num a -> Vect n a -> Vect n a -> Vect n a

588vAdd _ _ c (Nil _) (Nil _) = (Nil _)

589vAdd _ _ c ((::) _ _ x xs) ((::) _ _ y ys)

590 = (::) _ _ ((+) _ x y) (vAdd _ _ _ xs ys)

@@ -598,7 +598,7 @@ algorithm:

598

599\begin{SaveVerbatim}{vAddImpSolve}

600

601−vAdd : (a : Type) -> (n : Nat) -> Num a -> Vect a n -> Vect a n -> Vect a n

601+vAdd : (a : Type) -> (n : Nat) -> Num a -> Vect n a -> Vect n a -> Vect n a

602vAdd a O c (Nil a) (Nil a) = Nil a

603vAdd a (S k) c ((::) a k x xs) ((::) a k y ys)

604 = (::) a k ((+) c x y) (vAdd a k c xs ys)

@@ -614,14 +614,14 @@ syntax:

614\DM{

615\AR{

616\FN{vAdd} \Hab(\va\Hab\Type)\to(\vn\Hab\Nat)\to\TC{Num}\;\va\to

617− \Vect\;\va\;\vn\to\Vect\;\va\;\vn\to\Vect\;\va\;\vn\\

617+ \Vect\;\vn\;\va\to\Vect\;\vn\;\va\to\Vect\;\vn\;\va\\

618\RW{var}\;\va\Hab\Type,\;\vc\Hab\TC{Num}\;\va\SC\\

619\hg\FN{vAdd} \; \va \; \Z \; \vc \; (\DC{Nil}\;\va) \; (\DC{Nil}\;\va) \;

620\cq\;\DC{Nil}\;\va \\

621\RW{var}\;\AR{

622\va\Hab\Type,\;\vk\Hab\Nat,\;\vc\Hab\TC{Num}\;\va,\\

623−\vx\Hab\va,\;\vxs\Hab\Vect\;\va\;\vk,\;

623+\vx\Hab\va,\;\vxs\Hab\Vect\;\vk\;\va,\;

624−\vy\Hab\va,\;\vys\Hab\Vect\;\va\;\vk

624+\vy\Hab\va,\;\vys\Hab\Vect\;\vk\;\va

625\SC

626\\

627\FN{vAdd} \; \va \; (\suc\;\vk) \; \vc