9a5a45e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2816 from byorgey/tutorial-updates

Tutorial updates

commit9a5a45e1c9626c55fc87abae5c4930b88256e108 authorEdwin Brady <edwin.brady@gmail.com> dateSat 14 Nov 2015, 19:30 (11 years ago) parentbde101f c0063ff

3 files changed+29−14

compare with master

unifiedsplit

docs/tutorial/interp.rst+3−1 docs/tutorial/syntax.rst+3−3 docs/tutorial/typesfuns.rst+23−10

docs/tutorial/interp.rst+3−1

@@ -36,7 +36,9 @@ We’re going to define a representation of our language in such a way

3636that only well-typed programs can be represented. We’ll index the

3737representations of expressions by their type and the types of local

3838variables (the context), which we’ll be using regularly as an implicit

39−argument, so we define everything in a ``using`` block:

39+argument, so we define everything in a ``using`` block (keep in mind

40+that everything after this point needs to be indented so as to be

41+inside the ``using`` block):

4042

4143.. code-block:: idris

4244

docs/tutorial/syntax.rst+3−3

@@ -122,7 +122,7 @@ hard to program this way in practice. Recall the factorial program in

122122

123123 fact : Expr G (TyFun TyInt TyInt)

124124 fact = Lam (If (Op (==) (Var Stop) (Val 0))

125− (Val 1) (Op (*) (app fact (Op (-) (Var Stop) (Val 1)))

125+ (Val 1) (Op (*) (App fact (Op (-) (Var Stop) (Val 1)))

126126 (Var Stop)))

127127

128128Since this is a particularly useful pattern, Idris provides syntax

@@ -162,8 +162,8 @@ declaring:

162162

163163.. code-block:: idris

164164

165− (<$>) : (f : Lazy (Expr G (TyFun a t))) -> Expr G a -> Expr G t

166− (<$>) f a = App f a

165+ (<*>) : (f : Lazy (Expr G (TyFun a t))) -> Expr G a -> Expr G t

166+ (<*>) f a = App f a

167167

168168 pure : Expr G a -> Expr G a

169169 pure = id

docs/tutorial/typesfuns.rst+23−10

@@ -56,7 +56,7 @@ answer. For example:

5656::

5757

5858 *prims> 6*6+6

59− 42 : Int

59+ 42 : Integer

6060 *prims> x == 6*6+6

6161 True : Bool

6262

@@ -792,12 +792,12 @@ providing a default value:

792792

793793.. code-block:: idris

794794

795− maybe : Lazy b -> (a -> b) -> Maybe a -> b

795+ maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b

796796

797−Note that the type of the first argument is ``Lazy b`` rather than

798−simply ``b``. Since the default value might not be used, we mark it as

799−``Lazy`` in case it is a large expression where evaluating it then

800−discarding it would be wasteful.

797+Note that the types of the first two arguments are wrapped in

798+``Lazy``. Since only one of the two arguments will actually be used,

799+we mark them as ``Lazy`` in case they are large expressions where it

800+would be wasteful to compute and then discard them.

801801

802802Tuples

803803------

@@ -820,6 +820,15 @@ contain an arbitrary number of values, represented as nested pairs:

820820 jim : (String, Int, String)

821821 jim = ("Jim", 25, "Cambridge")

822822

823+::

824+

825+ *usefultypes> fst jim

826+ "Jim" : String

827+ *usefultypes> snd jim

828+ (25, "Cambridge") : (Int, String)

829+ *usefultypes> jim == ("Jim", (25, "Cambridge"))

830+ True : Bool

831+

823832Dependent Pairs

824833---------------

825834

@@ -1025,7 +1034,11 @@ For example:

10251034 className : String

10261035

10271036**Note** that it is no longer possible to use the ``addStudent``

1028−method from earlier as that would change the size of the class. To provide an add student the function must specify in the type that the size of the class has been increased by one. As the size if specified using natural numbers, the new value can be incremented using the successor constructor.

1037+function from earlier, since that would change the size of the class. A

1038+function to add a student must now specify in the type that the

1039+size of the class has been increased by one. As the size is specified

1040+using natural numbers, the new value can be incremented using the

1041+``S`` constructor.

10291042

10301043.. code-block:: idris

10311044

@@ -1137,8 +1150,8 @@ auxiliary functions, and is also used internally to implement pattern

11371150matching ``let`` and lambda bindings. It will *only* work if:

11381151

11391152- Each branch *matches* a value of the same type, and *returns* a

1140− value of the same type.

1153+ value of the same type.

11411154

11421155- The type of the result is "known". i.e. the type of the expression

1143− can be determined *without* type checking the ``case``-expression

1144− itself.

1156+ can be determined *without* type checking the ``case``-expression

1157+ itself.