git.iko.soy/Idris-dev
on master help sign in
Minor tutorial changes
ae47b8fEdwin Brady
tutorial/idris-tutorial.pdf
compare with master
unifiedsplit

Binary file not shown.

tutorial/interp.tex+6−5
@@ -1,6 +1,6 @@
1\section{Example: The Well-Typed Interpreter}
1\section{Example: The Well-Typed Interpreter}
2
2
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
4example, an interpreter for a simple functional programming language, with
4example, an interpreter for a simple functional programming language, with
5variables, function application, binary operators and an \texttt{if...then...else}
5variables, function application, binary operators and an \texttt{if...then...else}
6construct. We will use the dependent type system to ensure that any programs
6construct. We will use the dependent type system to ensure that any programs
@@ -16,13 +16,14 @@ data Ty = TyInt | TyBool | TyFun Ty Ty
16
16
17\noindent
17\noindent
18We can write a function to translate these representations to a concrete \Idris{}
18We 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:
20
21
21\begin{SaveVerbatim}{interpty}
22\begin{SaveVerbatim}{interpty}
22
23
23interpTy : Ty -> Set
24interpTy : Ty -> Set
24−interpTy TyInt = Int
25+interpTy TyInt = Int
25−interpTy TyBool = Bool
26+interpTy TyBool = Bool
26interpTy (TyFun A T) = interpTy A -> interpTy T
27interpTy (TyFun A T) = interpTy A -> interpTy T
27
28
28\end{SaveVerbatim}
29\end{SaveVerbatim}
@@ -338,7 +339,7 @@ at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
338$ idris interp.idr
339$ idris interp.idr
339 ____ __ _
340 ____ __ _
340 / _/___/ /____(_)____
341 / _/___/ /____(_)____
341− / // __ / ___/ / ___/ Version 0.9
342+ / // __ / ___/ / ___/ Version 0.9.0
342 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
343 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
343 /___/\__,_/_/ /_/____/ Type :? for help
344 /___/\__,_/_/ /_/____/ Type :? for help
344
345
tutorial/intro.tex+4−1
@@ -18,7 +18,10 @@ Correspondingly, the following values are examples of inhabitants of those types
18
18
19\noindent
19\noindent
20In a language with \emph{dependent types}, however, the distinction is less
20In a language with \emph{dependent types}, however, the distinction is less
21+clear.
21−clear. Dependent types allow types to ``depend'' on values. The standard
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
22example is the type of lists of a given length\footnote{Typically, and perhaps
25example is the type of lists of a given length\footnote{Typically, and perhaps
23confusingly, referred to in the dependently typed programming literature as
26confusingly, referred to in the dependently typed programming literature as
24``vectors''}, \texttt{Vect a n}, where \texttt{a} is the element type and
27``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
28\useverb{install}
28\useverb{install}
29
29
30\noindent
30\noindent
31−This will install the latest version released on Hackage\footnote{However version 0.9, which
31+This will install the latest version released on Hackage, along with any dependencies.
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.
34If, however, you would like the most up
32If, however, you would like the most up
35to date development version, you can find it on GitHub at
33to date development version, you can find it on GitHub at
36\url{https://github.com/edwinb/Idris-dev}.
34\url{https://github.com/edwinb/Idris-dev}.
@@ -84,7 +82,7 @@ environment. You should see something like the following:
84$ idris
82$ idris
85 ____ __ _
83 ____ __ _
86 / _/___/ /____(_)____
84 / _/___/ /____(_)____
87− / // __ / ___/ / ___/ Version 0.9
85+ / // __ / ___/ / ___/ Version 0.9.0
88 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
86 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
89 /___/\__,_/_/ /_/____/ Type :? for help
87 /___/\__,_/_/ /_/____/ Type :? for help
90
88
@@ -104,8 +102,8 @@ as shown in Figure \ref{cmds}. Figure \ref{run1} shows an example run in which
104the program is compiled to the executable \texttt{hello}.
102the program is compiled to the executable \texttt{hello}.
105
103
106\begin{SaveVerbatim}{cmds}
104\begin{SaveVerbatim}{cmds}
107−Idris version 0.9
105+Idris version 0.9.0
108−-----------------
106+-------------------
109
107
110 Command Arguments Purpose
108 Command Arguments Purpose
111
109
@@ -117,7 +115,7 @@ Idris version 0.9
117 :p :prove <name> Prove a metavariable
115 :p :prove <name> Prove a metavariable
118 :a :addproof Add last proof to source file
116 :a :addproof Add last proof to source file
119 :c :compile <filename> Compile to an executable <filename>
117 :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
121 :? :h :help Display this help text
119 :? :h :help Display this help text
122 :q :quit Exit the Idris system
120 :q :quit Exit the Idris system
123\end{SaveVerbatim}
121\end{SaveVerbatim}
@@ -129,7 +127,7 @@ Idris version 0.9
129$ idris hello.idr
127$ idris hello.idr
130 ____ __ _
128 ____ __ _
131 / _/___/ /____(_)____
129 / _/___/ /____(_)____
132− / // __ / ___/ / ___/ Version 0.9
130+ / // __ / ___/ / ___/ Version 0.9.0
133 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
131 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
134 /___/\__,_/_/ /_/____/ Type :? for help
132 /___/\__,_/_/ /_/____/ Type :? for help
135
133
tutorial/typesfuns.tex+3−4
@@ -34,7 +34,8 @@ quux = False
34An \Idris{} file consists of an optional module declaration (here
34An \Idris{} file consists of an optional module declaration (here
35\texttt{module prims}) followed by an optional list of imports (none here,
35\texttt{module prims}) followed by an optional list of imports (none here,
36however \Idris{} programs can consist of several modules, and the definitions
36however \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
38collection of declarations and definitions. Each definition must have a type
39collection of declarations and definitions. Each definition must have a type
39declaration (here, \texttt{x : Int}, \texttt{foo : String}, etc).
40declaration (here, \texttt{x : Int}, \texttt{foo : String}, etc).
40Indentation is significant --- a new declaration begins at the same leve
41Indentation 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:
74\subsection{Data Types}
75\subsection{Data Types}
75
76
76Data types are declared in a similar way to Haskell data types, with a similar
77Data 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:
80
79
81\begin{SaveVerbatim}{natlist}
80\begin{SaveVerbatim}{natlist}
82
81