@@ -1,8 +1,8 @@
11.. _sect-classes:
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,9 +241,9 @@ 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
250249``!``-notation
@@ -296,11 +295,11 @@ Monad comprehensions
296295
297296The list comprehension notation we saw in Section
298297:ref:`sect-more-expr` is more general, and applies to anything which
299−is an instance of both ``Monad`` and ``Alternative``:
298+has an implementation of both ``Monad`` and ``Alternative``:
300299
301300.. code-block:: idris
302301
303− class Applicative f => Alternative (f : Type -> Type) where
302+ interface Applicative f => Alternative (f : Type -> Type) where
304303 empty : f a
305304 (<|>) : f a -> f a -> f a
306305
@@ -364,19 +363,19 @@ alternative notion of function application, with explicit calls to
364363
365364Rather than having to insert ``m_app`` everywhere there is an
366365application, we can use idiom brackets to do the job for us.
367−To do this, we can make ``Maybe`` an instance of ``Applicative``
366+To do this, we can give ``Maybe`` an implementation of ``Applicative``
368367as follows, where ``<*>`` is defined in the same way as ``m_app``
369368above (this is defined in the Idris library):
370369
371370.. code-block:: idris
372371
373− instance Applicative Maybe where
372+ Applicative Maybe where
374373 pure = Just
375374
376375 (Just f) <*> (Just a) = Just (f a)
377376 _ <*> _ = Nothing
378377
379−Using ``<*>`` we can use this instance as follows, where a function
378+Using ``<*>`` we can use this implementation as follows, where a function
380379application ``[| f a1 …an |]`` is translated into ``pure f <*> a1 <*>
381380… <*> an``:
382381
@@ -407,8 +406,8 @@ We define a data type ``Eval`` to wrap an evaluator:
407406 data Eval : Type -> Type where
408407 MkEval : (List (String, Int) -> Maybe a) -> Eval a
409408
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
409+Wrapping the evaluator in a data type means we will be able to provide
410+implementations of interfaces for it later. We begin by defining a function to
412411retrieve values from the context during evaluation:
413412
414413.. code-block:: idris
@@ -421,18 +420,18 @@ retrieve values from the context during evaluation:
421420 then (Just val)
422421 else (fetchVal xs)
423422
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``:
423+When defining an evaluator for the language, we will be applying functions in
424+the context of an ``Eval``, so it is natural to give ``Eval`` an implementation
425+of ``Applicative``. Before ``Eval`` can have an implementation of
426+``Applicative`` it is necessary for ``Eval`` to have an implementation of
427+``Functor``:
429428
430429.. code-block:: idris
431430
432− instance Functor Eval where
431+ Functor Eval where
433432 map f (MkEval g) = MkEval (\e => map f (g e))
434433
435− instance Applicative Eval where
434+ Applicative Eval where
436435 pure x = MkEval (\e => Just x)
437436
438437 (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
@@ -454,24 +453,24 @@ to handle errors:
454453 runEval env e = case eval e of
455454 MkEval envFn => envFn env
456455
457−Named Instances
458−===============
456+Named Implementations
457+=====================
459458
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:
459+It can be desirable to have multiple implementations of an interface for the
460+same type, for example to provide alternative methods for sorting or printing
461+values. To achieve this, implementations can be *named* as follows:
463462
464463.. code-block:: idris
465464
466− instance [myord] Ord Nat where
465+ [myord] Ord Nat where
467466 compare Z (S n) = GT
468467 compare (S n) Z = LT
469468 compare Z Z = EQ
470469 compare (S x) (S y) = compare @{myord} x y
471470
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
471+This declares an implementation as normal, but with an explicit name,
472+``myord``. The syntax ``compare @{myord}`` gives an explicit implementation to
473+``compare``, otherwise it would use the default implementation for ``Nat``. We
475474can use this, for example, to sort a list of ``Nat`` in reverse.
476475Given the following list:
477476
@@ -480,35 +479,34 @@ Given the following list:
480479 testList : List Nat
481480 testList = [3,4,1]
482481
483−We can sort it using the default ``Ord`` instance, then the named
484−instance ``myord`` as follows, at the Idris prompt:
482+We can sort it using the default ``Ord`` implementation, then the named
483+implementation ``myord`` as follows, at the Idris prompt:
485484
486485::
487486
488− *named_instance> show (sort testList)
487+ *named_impl> show (sort testList)
489488 "[sO, sssO, ssssO]" : String
490− *named_instance> show (sort @{myord} testList)
489+ *named_impl> show (sort @{myord} testList)
491490 "[ssssO, sssO, sO]" : String
492491
493492
494493Determining Parameters
495494======================
496495
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:
496+When an interface has more than one parameter, it can help resolution if the
497+parameters used to find an implementation are restricted. For example:
500498
501499.. code-block:: idris
502500
503− class Monad m => MonadState s (m : Type -> Type) | m where
501+ interface Monad m => MonadState s (m : Type -> Type) | m where
504502 get : m s
505503 put : s -> m ()
506504
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.
505+In this interface, only ``m`` needs to be known to find an implementation of
506+this interface, and ``s`` can then be determined from the implementation. This
507+is declared with the ``| m`` after the interface declaration. We call ``m`` a
508+*determining parameter* of the ``MonadState`` interface, because it is the
509+parameter used to find an implementation.
512510
513511
514512.. [1] Conor McBride and Ross Paterson. 2008. Applicative programming