git.iko.soy/Idris-dev
on master help sign in
Minor tutorial changes
commitae47b8f8e8151f3cd4357d1ec04b12556dead956 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 12 Jan 2012, 19:03 (15 years ago) parent9538419
5 files changed+19−18
compare with master
unifiedsplit
tutorial/idris-tutorial.pdf tutorial/interp.tex+6−5 tutorial/intro.tex+4−1 tutorial/starting.tex+6−8 tutorial/typesfuns.tex+3−4
tutorial/idris-tutorial.pdf

Binary file not shown.

tutorial/interp.tex+6−5
@@ -1,6 +1,6 @@
11\section{Example: The Well-Typed Interpreter}
22
3−In this chapter, we'll use the features we've seen so far to write a larger
3+In this section, we'll use the features we've seen so far to write a larger
44example, an interpreter for a simple functional programming language, with
55variables, function application, binary operators and an \texttt{if...then...else}
66construct. We will use the dependent type system to ensure that any programs
@@ -16,13 +16,14 @@ data Ty = TyInt | TyBool | TyFun Ty Ty
1616
1717\noindent
1818We can write a function to translate these representations to a concrete \Idris{}
19−type:
19+type --- remember that types are first class, so can be calculated just like
20+any other value:
2021
2122\begin{SaveVerbatim}{interpty}
2223
2324interpTy : Ty -> Set
24−interpTy TyInt = Int
25−interpTy TyBool = Bool
25+interpTy TyInt = Int
26+interpTy TyBool = Bool
2627interpTy (TyFun A T) = interpTy A -> interpTy T
2728
2829\end{SaveVerbatim}
@@ -338,7 +339,7 @@ at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
338339$ idris interp.idr
339340 ____ __ _
340341 / _/___/ /____(_)____
341− / // __ / ___/ / ___/ Version 0.9
342+ / // __ / ___/ / ___/ Version 0.9.0
342343 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
343344 /___/\__,_/_/ /_/____/ Type :? for help
344345
tutorial/intro.tex+4−1
@@ -18,7 +18,10 @@ Correspondingly, the following values are examples of inhabitants of those types
1818
1919\noindent
2020In a language with \emph{dependent types}, however, the distinction is less
21−clear. Dependent types allow types to ``depend'' on values. The standard
21+clear.
22+Dependent types allow types to ``depend'' on values --- in other words,
23+types are a \emph{first class} language construct and can be manipulated like
24+any other value. The standard
2225example is the type of lists of a given length\footnote{Typically, and perhaps
2326confusingly, referred to in the dependently typed programming literature as
2427``vectors''}, \texttt{Vect a n}, where \texttt{a} is the element type and
tutorial/starting.tex+6−8
@@ -28,9 +28,7 @@ cabal install idris
2828\useverb{install}
2929
3030\noindent
31−This will install the latest version released on Hackage\footnote{However version 0.9, which
32−this tutorial describes, is not yet there, so don't do this. Finishing this tutorial is the
33−last requirement before releasing it :-).}, along with any dependencies.
31+This will install the latest version released on Hackage, along with any dependencies.
3432If, however, you would like the most up
3533to date development version, you can find it on GitHub at
3634\url{https://github.com/edwinb/Idris-dev}.
@@ -84,7 +82,7 @@ environment. You should see something like the following:
8482$ idris
8583 ____ __ _
8684 / _/___/ /____(_)____
87− / // __ / ___/ / ___/ Version 0.9
85+ / // __ / ___/ / ___/ Version 0.9.0
8886 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
8987 /___/\__,_/_/ /_/____/ Type :? for help
9088
@@ -104,8 +102,8 @@ as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which
104102the program is compiled to the executable \texttt{hello}.
105103
106104\begin{SaveVerbatim}{cmds}
107−Idris version 0.9
108−-----------------
105+Idris version 0.9.0
106+-------------------
109107
110108 Command Arguments Purpose
111109
@@ -117,7 +115,7 @@ Idris version 0.9
117115 :p :prove <name> Prove a metavariable
118116 :a :addproof Add last proof to source file
119117 :c :compile <filename> Compile to an executable <filename>
120− :exec :execute <filename> Compile to an executable <filename> and run
118+ :exec :execute Compile to an executable and run
121119 :? :h :help Display this help text
122120 :q :quit Exit the Idris system
123121\end{SaveVerbatim}
@@ -129,7 +127,7 @@ Idris version 0.9
129127$ idris hello.idr
130128 ____ __ _
131129 / _/___/ /____(_)____
132− / // __ / ___/ / ___/ Version 0.9
130+ / // __ / ___/ / ___/ Version 0.9.0
133131 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
134132 /___/\__,_/_/ /_/____/ Type :? for help
135133
tutorial/typesfuns.tex+3−4
@@ -34,7 +34,8 @@ quux = False
3434An \Idris{} file consists of an optional module declaration (here
3535\texttt{module prims}) followed by an optional list of imports (none here,
3636however \Idris{} programs can consist of several modules, and the definitions
37−in each module each have their own namespace, as we will discuss shortly) and a
37+in each module each have their own namespace, as we will discuss in Section
38+\ref{sect:namespaces}) and a
3839collection of declarations and definitions. Each definition must have a type
3940declaration (here, \texttt{x : Int}, \texttt{foo : String}, etc).
4041Indentation is significant --- a new declaration begins at the same leve
@@ -74,9 +75,7 @@ Boolean expressions can be tested with the \texttt{if...then...else} construct:
7475\subsection{Data Types}
7576
7677Data types are declared in a similar way to Haskell data types, with a similar
77−syntax. The main difference is that Idris syntax is not whitespace sensitive,
78−and declarations must end with a semi-colon. Natural numbers and lists, for
79−example, can be declared as follows:
78+syntax. Natural numbers and lists, for example, can be declared as follows:
8079
8180\begin{SaveVerbatim}{natlist}
8281