@@ -1,8 +1,8 @@
1−.. _sect-classes:
1+.. _sect-interfaces:
22
3−************
4−Type Classes
5−************
3+**********
4+Interfaces
5+**********
66
77We often want to define functions which work across several different
88data types. For example, we would like arithmetic operators to work on
@@ -10,34 +10,33 @@ data types. For example, we would like arithmetic operators to work on
1010``==`` to work on the majority of data types. We would like to be able
1111to display different types in a uniform way.
1212
13−To achieve this, we use a feature which has proved to be effective in
14−Haskell, namely *type classes*. To define a type class, we provide a
15−collection of overloaded operations which describe the interface for
16−*instances* of that class. A simple example is the ``Show`` type
17−class, which is defined in the prelude and provides an interface for
13+To achieve this, we use *interfaces*, which are similar to type classes in
14+Haskell or traits in Rust. To define an interface, we provide a collection of
15+overloadable functions. A simple example is the ``Show``
16+interface, which is defined in the prelude and provides an interface for
1817converting values to ``String``:
1918
2019.. code-block:: idris
2120
22− class Show a where
21+ interface Show a where
2322 show : a -> String
2423
2524This generates a function of the following type (which we call a
26−*method* of the ``Show`` class):
25+*method* of the ``Show`` interface):
2726
2827.. code-block:: idris
2928
3029 show : Show a => a -> String
3130
32−We can read this as: “under the constraint that ``a`` is an instance
33−of ``Show``, take an input ``a`` and return a ``String``.” An instance
34−of a class is defined with an ``instance`` declaration, which provides
35−implementations of the function for a specific type. For example, the
36−``Show`` instance for ``Nat`` could be defined as:
31+We can read this as: “under the constraint that ``a`` has an implementation
32+of ``Show``, take an input ``a`` and return a ``String``.” An implementation
33+of an interface is defined by giving definitions of the methods of the interface.
34+For example, the
35+``Show`` implementation for ``Nat`` could be defined as:
3736
3837.. code-block:: idris
3938
40− instance Show Nat where
39+ Show Nat where
4140 show Z = "Z"
4241 show (S k) = "s" ++ show k
4342
@@ -46,18 +45,18 @@ implementations of the function for a specific type. For example, the
4645 Idris> show (S (S (S Z)))
4746 "sssZ" : String
4847
49−Only one instance of a class can be given for a type — instances may
50−not overlap. Instance declarations can themselves have constraints.
51−To help with resolution, the arguments of an instance must be
48+Only one implementation of an interface can be given for a type — implementations may
49+not overlap. Implementation declarations can themselves have constraints.
50+To help with resolution, the arguments of an implementation must be
5251constructors (either data or type constructors), variables or
53−constants (i.e. you cannot give an instance for a function). For
54−example, to define a ``Show`` instance for vectors, we need to know
55−that there is a ``Show`` instance for the element type, because we are
52+constants (i.e. you cannot give an implementation for a function). For
53+example, to define a ``Show`` implementation for vectors, we need to know
54+that there is a ``Show`` implementation for the element type, because we are
5655going to use it to convert each element to a ``String``:
5756
5857.. code-block:: idris
5958
60− instance Show a => Show (Vect n a) where
59+ Show a => Show (Vect n a) where
6160 show xs = "[" ++ show' xs ++ "]" where
6261 show' : Vect n a -> String
6362 show' Nil = ""
@@ -67,22 +66,22 @@ going to use it to convert each element to a ``String``:
6766Default Definitions
6867===================
6968
70−The library defines an ``Eq`` class which provides an interface for
71−comparing values for equality or inequality, with instances for all of
69+The library defines an ``Eq`` interface which provides methods for
70+comparing values for equality or inequality, with implementations for all of
7271the built-in types:
7372
7473.. code-block:: idris
7574
76− class Eq a where
75+ interface Eq a where
7776 (==) : a -> a -> Bool
7877 (/=) : a -> a -> Bool
7978
80−To declare an instance of a type, we have to give definitions of all
81−of the methods. For example, for an instance of ``Eq`` for ``Nat``:
79+To declare an implementation for a type, we have to give definitions of all
80+of the methods. For example, for an implementation of ``Eq`` for ``Nat``:
8281
8382.. code-block:: idris
8483
85− instance Eq Nat where
84+ Eq Nat where
8685 Z == Z = True
8786 (S x) == (S y) = x == y
8887 Z == (S y) = False
@@ -93,28 +92,28 @@ of the methods. For example, for an instance of ``Eq`` for ``Nat``:
9392It is hard to imagine many cases where the ``/=`` method will be
9493anything other than the negation of the result of applying the ``==``
9594method. It is therefore convenient to give a default definition for
96−each method in the class declaration, in terms of the other method:
95+each method in the interface declaration, in terms of the other method:
9796
9897.. code-block:: idris
9998
100− class Eq a where
99+ interface Eq a where
101100 (==) : a -> a -> Bool
102101 (/=) : a -> a -> Bool
103102
104103 x /= y = not (x == y)
105104 x == y = not (x /= y)
106105
107−A minimal complete definition of an ``Eq`` instance requires either
106+A minimal complete implementation of ``Eq`` requires either
108107``==`` or ``/=`` to be defined, but does not require both. If a method
109108definition is missing, and there is a default definition for it, then
110109the default is used instead.
111110
112−Extending Classes
113−=================
111+Extending Interfaces
112+====================
114113
115−Classes can also be extended. A logical next step from an equality
114+Interfaces can also be extended. A logical next step from an equality
116115relation ``Eq`` is to define an ordering relation ``Ord``. We can
117−define an ``Ord`` class which inherits methods from ``Eq`` as well as
116+define an ``Ord`` interface which inherits methods from ``Eq`` as well as
118117defining some of its own:
119118
120119.. code-block:: idris
@@ -123,7 +122,7 @@ defining some of its own:
123122
124123.. code-block:: idris
125124
126− class Eq a => Ord a where
125+ interface Eq a => Ord a where
127126 compare : a -> a -> Ordering
128127
129128 (<) : a -> a -> Bool
@@ -133,11 +132,11 @@ defining some of its own:
133132 max : a -> a -> a
134133 min : a -> a -> a
135134
136−The ``Ord`` class allows us to compare two values and determine their
135+The ``Ord`` interface allows us to compare two values and determine their
137136ordering. Only the ``compare`` method is required; every other method
138137has a default definition. Using this we can write functions such as
139138``sort``, a function which sorts a list into increasing order,
140−provided that the element type of the list is in the ``Ord`` class. We
139+provided that the element type of the list is in the ``Ord`` interface. We
141140give the constraints on the type variables left of the fat arrow
142141``=>``, and the function type to the right of the fat arrow:
143142
@@ -145,7 +144,7 @@ give the constraints on the type variables left of the fat arrow
145144
146145 sort : Ord a => List a -> List a
147146
148−Functions, classes and instances can have multiple
147+Functions, interfaces and implementations can have multiple
149148constraints. Multiple constraints are written in brackets in a comma
150149separated list, for example:
151150
@@ -157,16 +156,16 @@ separated list, for example:
157156Functors and Applicatives
158157=========================
159158
160−So far, we have seen single parameter type classes, where the parameter
161−is of type ``Type``. In general, there can be any number (greater than
162−0) of parameters, and the parameters can have *any* type. If the type
159+So far, we have seen single parameter interfaces, where the parameter
160+is of type ``Type``. In general, there can be any number of parameters
161+(even zero), and the parameters can have *any* type. If the type
163162of the parameter is not ``Type``, we need to give an explicit type
164−declaration. For example, the ``Functor`` class is defined in the
165−library:
163+declaration. For example, the ``Functor`` interface is defined in the
164+prelude:
166165
167166.. code-block:: idris
168167
169− class Functor (f : Type -> Type) where
168+ interface Functor (f : Type -> Type) where
170169 map : (m : a -> b) -> f a -> f b
171170
172171A functor allows a function to be applied across a structure, for
@@ -174,7 +173,7 @@ example to apply a function to every element in a ``List``:
174173
175174.. code-block:: idris
176175
177− instance Functor List where
176+ Functor List where
178177 map f [] = []
179178 map f (x::xs) = f x :: map f xs
180179
@@ -190,21 +189,21 @@ abstracts the notion of function application:
190189
191190 infixl 2 <*>
192191
193− class Functor f => Applicative (f : Type -> Type) where
192+ interface Functor f => Applicative (f : Type -> Type) where
194193 pure : a -> f a
195194 (<*>) : f (a -> b) -> f a -> f b
196195
197196Monads and ``do``-notation
198197==========================
199198
200−The ``Monad`` class allows us to encapsulate binding and computation,
199+The ``Monad`` interface allows us to encapsulate binding and computation,
201200and is the basis of ``do``-notation introduced in Section
202201:ref:`sect-do`. It extends ``Applicative`` as defined above, and is
203202defined as follows:
204203
205204.. code-block:: idris
206205
207− class Applicative m => Monad (m : Type -> Type) where
206+ interface Applicative m => Monad (m : Type -> Type) where
208207 (>>=) : m a -> (a -> m b) -> m b
209208
210209Inside a ``do`` block, the following syntactic transformations are
@@ -216,12 +215,12 @@ applied:
216215
217216- ``let x = v; e`` becomes ``let x = v in e``
218217
219−``IO`` is an instance of ``Monad``, defined using primitive functions.
220−We can also define an instance for ``Maybe``, as follows:
218+``IO`` has an implementation of ``Monad``, defined using primitive functions.
219+We can also define an implementation for ``Maybe``, as follows:
221220
222221.. code-block:: idris
223222
224− instance Monad Maybe where
223+ Monad Maybe where
225224 Nothing >>= k = Nothing
226225 (Just x) >>= k = k x
227226
@@ -242,11 +241,75 @@ are both available, or return ``Nothing`` if one or both are not ("fail fast").
242241
243242::
244243
245− *classes> m_add (Just 20) (Just 22)
244+ *ifaces> m_add (Just 20) (Just 22)
246245 Just 42 : Maybe Int
247− *classes> m_add (Just 20) Nothing
246+ *ifaces> m_add (Just 20) Nothing
248247 Nothing : Maybe Int
249248
249+Pattern Matching Bind
250+---------------------
251+
252+Sometimes we want to pattern match immediately on the result of a function
253+in ``do`` notation. For example, let's say we have a function ``readNumber``
254+which reads a number from the console, returning a value of the form
255+``Just x`` if the number is valid, or ``Nothing`` otherwise:
256+
257+.. code-block:: idris
258+
259+ readNumber : IO (Maybe Nat)
260+ readNumber = do
261+ input <- getLine
262+ if all isDigit (unpack input)
263+ then pure (Just (cast input))
264+ else pure Nothing
265+
266+If we then use it to write a function to read two numbers, returning
267+``Nothing`` if neither are valid, then we would like to pattern match
268+on the result of ``readNumber``:
269+
270+.. code-block:: idris
271+
272+ readNumbers : IO (Maybe (Nat, Nat))
273+ readNumbers =
274+ do x <- readNumber
275+ case x of
276+ Nothing => pure Nothing
277+ Just x_ok => do y <- readNumber
278+ case y of
279+ Nothing => pure Nothing
280+ Just y_ok => pure (Just (x_ok, y_ok))
281+
282+If there's a lot of error handling, this could get deeply nested very quickly!
283+So instead, we can combine the bind and the pattern match in one line. For example,
284+we could try pattern matching on values of the form ``Just x_ok``:
285+
286+.. code-block:: idris
287+
288+ readNumbers : IO (Maybe (Nat, Nat))
289+ readNumbers =
290+ do Just x_ok <- readNumber
291+ Just y_ok <- readNumber
292+ pure (Just (x_ok, y_ok))
293+
294+There is still a problem, however, because we've now omitted the case for
295+``Nothing`` so ``readNumbers`` is no longer total! We can add the ``Nothing``
296+case back as follows:
297+
298+.. code-block:: idris
299+
300+ readNumbers : IO (Maybe (Nat, Nat))
301+ readNumbers =
302+ do Just x_ok <- readNumber | Nothing => pure Nothing
303+ Just y_ok <- readNumber | Nothing => pure Nothing
304+ pure (Just (x_ok, y_ok))
305+
306+The effect of this version of ``readNumbers`` is identical to the first (in
307+fact, it is syntactic sugar for it and directly translated back into that form).
308+The first part of each statement (``Just x_ok <-`` and ``Just y_ok <-``) gives
309+the preferred binding - if this matches, execution will continue with the rest
310+of the ``do`` block. The second part gives the alternative bindings, of which
311+there may be more than one.
312+
250313``!``-notation
251314--------------
252315
@@ -296,11 +359,11 @@ Monad comprehensions
296359
297360The list comprehension notation we saw in Section
298361:ref:`sect-more-expr` is more general, and applies to anything which
299−is an instance of both ``Monad`` and ``Alternative``:
362+has an implementation of both ``Monad`` and ``Alternative``:
300363
301364.. code-block:: idris
302365
303− class Applicative f => Alternative (f : Type -> Type) where
366+ interface Applicative f => Alternative (f : Type -> Type) where
304367 empty : f a
305368 (<|>) : f a -> f a -> f a
306369
@@ -364,19 +427,19 @@ alternative notion of function application, with explicit calls to
364427
365428Rather than having to insert ``m_app`` everywhere there is an
366429application, we can use idiom brackets to do the job for us.
367−To do this, we can make ``Maybe`` an instance of ``Applicative``
430+To do this, we can give ``Maybe`` an implementation of ``Applicative``
368431as follows, where ``<*>`` is defined in the same way as ``m_app``
369432above (this is defined in the Idris library):
370433
371434.. code-block:: idris
372435
373− instance Applicative Maybe where
436+ Applicative Maybe where
374437 pure = Just
375438
376439 (Just f) <*> (Just a) = Just (f a)
377440 _ <*> _ = Nothing
378441
379−Using ``<*>`` we can use this instance as follows, where a function
442+Using ``<*>`` we can use this implementation as follows, where a function
380443application ``[| f a1 …an |]`` is translated into ``pure f <*> a1 <*>
381444… <*> an``:
382445
@@ -407,8 +470,8 @@ We define a data type ``Eval`` to wrap an evaluator:
407470 data Eval : Type -> Type where
408471 MkEval : (List (String, Int) -> Maybe a) -> Eval a
409472
410−Wrapping the evaluator in a data type means we will be able to make it
411−an instance of a type class later. We begin by defining a function to
473+Wrapping the evaluator in a data type means we will be able to provide
474+implementations of interfaces for it later. We begin by defining a function to
412475retrieve values from the context during evaluation:
413476
414477.. code-block:: idris
@@ -421,18 +484,18 @@ retrieve values from the context during evaluation:
421484 then (Just val)
422485 else (fetchVal xs)
423486
424−When defining an evaluator for the language, we will be applying
425−functions in the context of an ``Eval``, so it is natural to make
426−``Eval`` an instance of ``Applicative``. Before ``Eval`` can be an
427−instance of ``Applicative`` it is necessary to make ``Eval`` an
428−instance of ``Functor``:
487+When defining an evaluator for the language, we will be applying functions in
488+the context of an ``Eval``, so it is natural to give ``Eval`` an implementation
489+of ``Applicative``. Before ``Eval`` can have an implementation of
490+``Applicative`` it is necessary for ``Eval`` to have an implementation of
491+``Functor``:
429492
430493.. code-block:: idris
431494
432− instance Functor Eval where
495+ Functor Eval where
433496 map f (MkEval g) = MkEval (\e => map f (g e))
434497
435− instance Applicative Eval where
498+ Applicative Eval where
436499 pure x = MkEval (\e => Just x)
437500
438501 (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
@@ -454,24 +517,24 @@ to handle errors:
454517 runEval env e = case eval e of
455518 MkEval envFn => envFn env
456519
457−Named Instances
458−===============
520+Named Implementations
521+=====================
459522
460−It can be desirable to have multiple instances of a type class, for
461−example to provide alternative methods for sorting or printing values.
462−To achieve this, instances can be *named* as follows:
523+It can be desirable to have multiple implementations of an interface for the
524+same type, for example to provide alternative methods for sorting or printing
525+values. To achieve this, implementations can be *named* as follows:
463526
464527.. code-block:: idris
465528
466− instance [myord] Ord Nat where
529+ [myord] Ord Nat where
467530 compare Z (S n) = GT
468531 compare (S n) Z = LT
469532 compare Z Z = EQ
470533 compare (S x) (S y) = compare @{myord} x y
471534
472−This declares an instance as normal, but with an explicit name,
473−``myord``. The syntax ``compare @{myord}`` gives an explicit instance to
474−``compare``, otherwise it would use the default instance for ``Nat``. We
535+This declares an implementation as normal, but with an explicit name,
536+``myord``. The syntax ``compare @{myord}`` gives an explicit implementation to
537+``compare``, otherwise it would use the default implementation for ``Nat``. We
475538can use this, for example, to sort a list of ``Nat`` in reverse.
476539Given the following list:
477540
@@ -480,35 +543,34 @@ Given the following list:
480543 testList : List Nat
481544 testList = [3,4,1]
482545
483−We can sort it using the default ``Ord`` instance, then the named
484−instance ``myord`` as follows, at the Idris prompt:
546+We can sort it using the default ``Ord`` implementation, then the named
547+implementation ``myord`` as follows, at the Idris prompt:
485548
486549::
487550
488− *named_instance> show (sort testList)
551+ *named_impl> show (sort testList)
489552 "[sO, sssO, ssssO]" : String
490− *named_instance> show (sort @{myord} testList)
553+ *named_impl> show (sort @{myord} testList)
491554 "[ssssO, sssO, sO]" : String
492555
493556
494557Determining Parameters
495558======================
496559
497−When a class has more than one parameter, it can help resolution if
498−the parameters used to resolve the type class are restricted. For
499−example:
560+When an interface has more than one parameter, it can help resolution if the
561+parameters used to find an implementation are restricted. For example:
500562
501563.. code-block:: idris
502564
503− class Monad m => MonadState s (m : Type -> Type) | m where
565+ interface Monad m => MonadState s (m : Type -> Type) | m where
504566 get : m s
505567 put : s -> m ()
506568
507−In this class, only ``m`` needs to be known to resolve this class, and
508−``s`` can then be determined from the instance. This is declared with
509−the ``| m`` after the class declaration. We call ``m`` a *determining
510−parameter* of the ``MonadState`` class, because it is the parameter
511−used to resolve an instance.
569+In this interface, only ``m`` needs to be known to find an implementation of
570+this interface, and ``s`` can then be determined from the implementation. This
571+is declared with the ``| m`` after the interface declaration. We call ``m`` a
572+*determining parameter* of the ``MonadState`` interface, because it is the
573+parameter used to find an implementation.
512574
513575
514576.. [1] Conor McBride and Ross Paterson. 2008. Applicative programming