1862197 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Switch Vect arguments in implementation paper

commit18621973c31e6e54633bd4a9b8acf5c9838aa3b7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 28 Jul 2013, 14:01 (13 years ago) parent7a28778

5 files changed+47−47

compare with master

unifiedsplit

papers/impl-paper/elaboration.tex+11−11 papers/impl-paper/hll.tex+22−22 papers/impl-paper/intro.tex+4−4 papers/impl-paper/library.ltx+1−1 papers/impl-paper/typechecking.tex+9−9

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

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

457457

458458\DM{

459459\AR{

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

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

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

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

462462\\

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

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

464464}

465465}

466466

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

481481\DM{

482482\AR{

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

485485\\

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

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

487487}

488488}

489489

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

895895

896896\begin{SaveVerbatim}{vAddImpT}

897897

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

899899

900900\end{SaveVerbatim}

901901\useverb{vAddImpT}

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

907907\begin{SaveVerbatim}{vAddImpT}

908908

909909vAdd : (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

911911

912912\end{SaveVerbatim}

913913\useverb{vAddImpT}

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

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

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

10181018arguments in types bound explicitly

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

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

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

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

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

10221022only appear in top level declarations.

10231023It is in general straightforward to

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

18161816

18171817\begin{SaveVerbatim}{vappmv}

18181818

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

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

18201820Nil ++ ys = ys

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

18221822

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

18321832

18331833*vec> :t append_rec

18341834append_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

18361836

18371837\end{SaveVerbatim}

18381838\useverb{appendrec}

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

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

5656

5757\begin{SaveVerbatim}{natlist}

5858

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

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

6060 -- (zero and successor)

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

6262

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

181181

182182\begin{SaveVerbatim}{vect}

183183

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

185− Nil : Vect a O

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

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

185+ Nil : Vect Z a

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

187187

188188\end{SaveVerbatim}

189189\useverb{vect}

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

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

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

201201GADT declaration: it explicitly states the type

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

203−argument, 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}.

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

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

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

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

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

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

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

209209vectors 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})

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

212212

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

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

218218

219219\begin{SaveVerbatim}{vapp}

220220

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

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

222222Nil ++ ys = ys

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

224224

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

233233\begin{SaveVerbatim}{findecl}

234234

235235data Fin : Nat -> Type where

236− fO : Fin (S k)

236+ fZ : Fin (S k)

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

238238

239239\end{SaveVerbatim}

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

241241

242242\noindent

243243This 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;

245245\texttt{fS n} as the

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

247247\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:

259259

260260\begin{SaveVerbatim}{vindex}

261261

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

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

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

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

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

265265

266266\end{SaveVerbatim}

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

284284

285285\begin{SaveVerbatim}{vindexty}

286286

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

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

288288

289289\end{SaveVerbatim}

290290\useverb{vindexty}

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

297297

298298\begin{SaveVerbatim}{vindeximppl}

299299

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

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

301301

302302\end{SaveVerbatim}

303303\useverb{vindeximppl}

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

308308

309309\begin{SaveVerbatim}{vindeximpty}

310310

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

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

312312

313313\end{SaveVerbatim}

314314\useverb{vindeximpty}

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

316316\noindent

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

318318not 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

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

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

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

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

335335

336336\begin{SaveVerbatim}{vindexn}

337337

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

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

339339

340340\end{SaveVerbatim}

341341\useverb{vindexn}

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

359359

360360\begin{SaveVerbatim}{vadd}

361361

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

363363vAdd [] [] = []

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

365365

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

450450

451451\begin{SaveVerbatim}{showvec}

452452

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

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

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

455− show' : Vect a n -> String

455+ show' : Vect n a -> String

456456 show' Nil = ""

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

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

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

570570

571571\begin{SaveVerbatim}{appdep}

572572

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

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

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

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

576576

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

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

109109

110110\begin{SaveVerbatim}{vadd}

111111

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

113113vAdd [] [] = []

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

115115

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

143143\DM{

144144\AR{

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

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

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

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

150150\RW{var}\;\AR{

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

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

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

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

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

154154\SC

155155\\

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

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

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

142142

143143\newcommand{\NatPackage}{

144144 \newcommand{\Nat}{\TC{Nat}}

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

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

146146 \newcommand{\suc}{\DC{S}}

147147 \newcommand{\NatDecl}{

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

285285

286286\DM{

287287\AR{

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

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

289289\hg\hg

290290\ARd{

291291& \nil\Hab\List\;\va\\

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

304304

305305\DM{

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

308308\hg\hg\ARd{

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

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

310310\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}}

312312}

313313}

314314}

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

584584

585585\begin{SaveVerbatim}{vAddImp}

586586

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

588588vAdd _ _ c (Nil _) (Nil _) = (Nil _)

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

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

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

598598

599599\begin{SaveVerbatim}{vAddImpSolve}

600600

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

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

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

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

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

614614\DM{

615615\AR{

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

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

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

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

621621\RW{var}\;\AR{

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

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

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

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

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

625625\SC

626626\\

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