@@ -1,8 +1,8 @@
1.. _sect-classes:
1.. _sect-classes:
3−************
3+**********
4−Type Classes
4+Interfaces
5−************
5+**********
7We often want to define functions which work across several different
7We often want to define functions which work across several different
8data types. For example, we would like arithmetic operators to work on
8data 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
10``==`` to work on the majority of data types. We would like to be able
10``==`` to work on the majority of data types. We would like to be able
11to display different types in a uniform way.
11to display different types in a uniform way.
13−To achieve this, we use a feature which has proved to be effective in
13+To achieve this, we use *interfaces*, which are similar to type classes in
14−Haskell, namely *type classes*. To define a type class, we provide a
14+Haskell or traits in Rust. To define an interface, we provide a collection of
15−collection of overloaded operations which describe the interface for
16−*instances* of that class. A simple example is the ``Show`` type
15+overloadable functions. A simple example is the ``Show``
17−class, which is defined in the prelude and provides an interface for
16+interface, which is defined in the prelude and provides an interface for
18converting values to ``String``:
17converting values to ``String``:
20.. code-block:: idris
19.. code-block:: idris
22− class Show a where
21+ interface Show a where
23 show : a -> String
22 show : a -> String
25This generates a function of the following type (which we call a
24This generates a function of the following type (which we call a
26−*method* of the ``Show`` class):
25+*method* of the ``Show`` interface):
28.. code-block:: idris
27.. code-block:: idris
30 show : Show a => a -> String
29 show : Show a => a -> String
32−We can read this as: “under the constraint that ``a`` is an instance
31+We can read this as: “under the constraint that ``a`` has an implementation
33−of ``Show``, take an input ``a`` and return a ``String``.” An instance
32+of ``Show``, take an input ``a`` and return a ``String``.” An implementation
34−of a class is defined with an ``instance`` declaration, which provides
33+of an interface is defined by giving definitions of the methods of the interface.
35−implementations of the function for a specific type. For example, the
34+For example, the
36−``Show`` instance for ``Nat`` could be defined as:
35+``Show`` implementation for ``Nat`` could be defined as:
38.. code-block:: idris
37.. code-block:: idris
40− instance Show Nat where
39+ Show Nat where
41 show Z = "Z"
40 show Z = "Z"
42 show (S k) = "s" ++ show k
41 show (S k) = "s" ++ show k
@@ -46,18 +45,18 @@ implementations of the function for a specific type. For example, the
46 Idris> show (S (S (S Z)))
45 Idris> show (S (S (S Z)))
47 "sssZ" : String
46 "sssZ" : String
49−Only one instance of a class can be given for a type — instances may
48+Only one implementation of an interface can be given for a type — implementations may
50−not overlap. Instance declarations can themselves have constraints.
49+not overlap. Implementation declarations can themselves have constraints.
51−To help with resolution, the arguments of an instance must be
50+To help with resolution, the arguments of an implementation must be
52constructors (either data or type constructors), variables or
51constructors (either data or type constructors), variables or
53−constants (i.e. you cannot give an instance for a function). For
52+constants (i.e. you cannot give an implementation for a function). For
54−example, to define a ``Show`` instance for vectors, we need to know
53+example, to define a ``Show`` implementation for vectors, we need to know
55−that there is a ``Show`` instance for the element type, because we are
54+that there is a ``Show`` implementation for the element type, because we are
56going to use it to convert each element to a ``String``:
55going to use it to convert each element to a ``String``:
58.. code-block:: idris
57.. code-block:: idris
60− instance Show a => Show (Vect n a) where
59+ Show a => Show (Vect n a) where
61 show xs = "[" ++ show' xs ++ "]" where
60 show xs = "[" ++ show' xs ++ "]" where
62 show' : Vect n a -> String
61 show' : Vect n a -> String
63 show' Nil = ""
62 show' Nil = ""
@@ -67,22 +66,22 @@ going to use it to convert each element to a ``String``:
67Default Definitions
66Default Definitions
68===================
67===================
70−The library defines an ``Eq`` class which provides an interface for
69+The library defines an ``Eq`` interface which provides methods for
71−comparing values for equality or inequality, with instances for all of
70+comparing values for equality or inequality, with implementations for all of
72the built-in types:
71the built-in types:
74.. code-block:: idris
73.. code-block:: idris
76− class Eq a where
75+ interface Eq a where
77 (==) : a -> a -> Bool
76 (==) : a -> a -> Bool
78 (/=) : a -> a -> Bool
77 (/=) : a -> a -> Bool
80−To declare an instance of a type, we have to give definitions of all
79+To declare an implementation for a type, we have to give definitions of all
81−of the methods. For example, for an instance of ``Eq`` for ``Nat``:
80+of the methods. For example, for an implementation of ``Eq`` for ``Nat``:
83.. code-block:: idris
82.. code-block:: idris
85− instance Eq Nat where
84+ Eq Nat where
86 Z == Z = True
85 Z == Z = True
87 (S x) == (S y) = x == y
86 (S x) == (S y) = x == y
88 Z == (S y) = False
87 Z == (S y) = False
@@ -93,28 +92,28 @@ of the methods. For example, for an instance of ``Eq`` for ``Nat``:
93It is hard to imagine many cases where the ``/=`` method will be
92It is hard to imagine many cases where the ``/=`` method will be
94anything other than the negation of the result of applying the ``==``
93anything other than the negation of the result of applying the ``==``
95method. It is therefore convenient to give a default definition for
94method. 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:
98.. code-block:: idris
97.. code-block:: idris
100− class Eq a where
99+ interface Eq a where
101 (==) : a -> a -> Bool
100 (==) : a -> a -> Bool
102 (/=) : a -> a -> Bool
101 (/=) : a -> a -> Bool
104 x /= y = not (x == y)
103 x /= y = not (x == y)
105 x == y = not (x /= y)
104 x == y = not (x /= y)
107−A minimal complete definition of an ``Eq`` instance requires either
106+A minimal complete implementation of ``Eq`` requires either
108``==`` or ``/=`` to be defined, but does not require both. If a method
107``==`` or ``/=`` to be defined, but does not require both. If a method
109definition is missing, and there is a default definition for it, then
108definition is missing, and there is a default definition for it, then
110the default is used instead.
109the default is used instead.
112−Extending Classes
111+Extending Interfaces
113−=================
112+====================
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
116relation ``Eq`` is to define an ordering relation ``Ord``. We can
115relation ``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
118defining some of its own:
117defining some of its own:
120.. code-block:: idris
119.. code-block:: idris
@@ -123,7 +122,7 @@ defining some of its own:
124.. code-block:: idris
123.. code-block:: idris
126− class Eq a => Ord a where
125+ interface Eq a => Ord a where
127 compare : a -> a -> Ordering
126 compare : a -> a -> Ordering
129 (<) : a -> a -> Bool
128 (<) : a -> a -> Bool
@@ -133,11 +132,11 @@ defining some of its own:
133 max : a -> a -> a
132 max : a -> a -> a
134 min : a -> a -> a
133 min : a -> a -> a
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
137ordering. Only the ``compare`` method is required; every other method
136ordering. Only the ``compare`` method is required; every other method
138has a default definition. Using this we can write functions such as
137has a default definition. Using this we can write functions such as
139``sort``, a function which sorts a list into increasing order,
138``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
141give the constraints on the type variables left of the fat arrow
140give the constraints on the type variables left of the fat arrow
142``=>``, and the function type to the right of the fat arrow:
141``=>``, and the function type to the right of the fat arrow:
@@ -145,7 +144,7 @@ give the constraints on the type variables left of the fat arrow
146 sort : Ord a => List a -> List a
145 sort : Ord a => List a -> List a
148−Functions, classes and instances can have multiple
147+Functions, interfaces and implementations can have multiple
149constraints. Multiple constraints are written in brackets in a comma
148constraints. Multiple constraints are written in brackets in a comma
150separated list, for example:
149separated list, for example:
@@ -157,16 +156,16 @@ separated list, for example:
157Functors and Applicatives
156Functors and Applicatives
158=========================
157=========================
160−So far, we have seen single parameter type classes, where the parameter
159+So far, we have seen single parameter interfaces, where the parameter
161−is of type ``Type``. In general, there can be any number (greater than
160+is of type ``Type``. In general, there can be any number of parameters
162−0) of parameters, and the parameters can have *any* type. If the type
161+(even zero), and the parameters can have *any* type. If the type
163of the parameter is not ``Type``, we need to give an explicit type
162of the parameter is not ``Type``, we need to give an explicit type
164−declaration. For example, the ``Functor`` class is defined in the
163+declaration. For example, the ``Functor`` interface is defined in the
167.. code-block:: idris
166.. code-block:: idris
169− class Functor (f : Type -> Type) where
168+ interface Functor (f : Type -> Type) where
170 map : (m : a -> b) -> f a -> f b
169 map : (m : a -> b) -> f a -> f b
172A functor allows a function to be applied across a structure, for
171A 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``:
175.. code-block:: idris
174.. code-block:: idris
177− instance Functor List where
176+ Functor List where
178 map f [] = []
177 map f [] = []
179 map f (x::xs) = f x :: map f xs
178 map f (x::xs) = f x :: map f xs
@@ -190,21 +189,21 @@ abstracts the notion of function application:
191 infixl 2 <*>
190 infixl 2 <*>
193− class Functor f => Applicative (f : Type -> Type) where
192+ interface Functor f => Applicative (f : Type -> Type) where
194 pure : a -> f a
193 pure : a -> f a
195 (<*>) : f (a -> b) -> f a -> f b
194 (<*>) : f (a -> b) -> f a -> f b
197Monads and ``do``-notation
196Monads and ``do``-notation
198==========================
197==========================
200−The ``Monad`` class allows us to encapsulate binding and computation,
199+The ``Monad`` interface allows us to encapsulate binding and computation,
201and is the basis of ``do``-notation introduced in Section
200and is the basis of ``do``-notation introduced in Section
202:ref:`sect-do`. It extends ``Applicative`` as defined above, and is
201:ref:`sect-do`. It extends ``Applicative`` as defined above, and is
203defined as follows:
202defined as follows:
205.. code-block:: idris
204.. code-block:: idris
207− class Applicative m => Monad (m : Type -> Type) where
206+ interface Applicative m => Monad (m : Type -> Type) where
208 (>>=) : m a -> (a -> m b) -> m b
207 (>>=) : m a -> (a -> m b) -> m b
210Inside a ``do`` block, the following syntactic transformations are
209Inside a ``do`` block, the following syntactic transformations are
@@ -216,12 +215,12 @@ applied:
217- ``let x = v; e`` becomes ``let x = v in e``
216- ``let x = v; e`` becomes ``let x = v in e``
219−``IO`` is an instance of ``Monad``, defined using primitive functions.
218+``IO`` has an implementation of ``Monad``, defined using primitive functions.
220−We can also define an instance for ``Maybe``, as follows:
219+We can also define an implementation for ``Maybe``, as follows:
222.. code-block:: idris
221.. code-block:: idris
224− instance Monad Maybe where
223+ Monad Maybe where
225 Nothing >>= k = Nothing
224 Nothing >>= k = Nothing
226 (Just x) >>= k = k x
225 (Just x) >>= k = k x
@@ -242,9 +241,9 @@ are both available, or return ``Nothing`` if one or both are not ("fail fast").
245− *classes> m_add (Just 20) (Just 22)
244+ *ifaces> m_add (Just 20) (Just 22)
246 Just 42 : Maybe Int
245 Just 42 : Maybe Int
247− *classes> m_add (Just 20) Nothing
246+ *ifaces> m_add (Just 20) Nothing
248 Nothing : Maybe Int
247 Nothing : Maybe Int
250``!``-notation
249``!``-notation
@@ -296,11 +295,11 @@ Monad comprehensions
297The list comprehension notation we saw in Section
296The list comprehension notation we saw in Section
298:ref:`sect-more-expr` is more general, and applies to anything which
297: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``:
301.. code-block:: idris
300.. code-block:: idris
303− class Applicative f => Alternative (f : Type -> Type) where
302+ interface Applicative f => Alternative (f : Type -> Type) where
304 empty : f a
303 empty : f a
305 (<|>) : f a -> f a -> f a
304 (<|>) : f a -> f a -> f a
@@ -364,19 +363,19 @@ alternative notion of function application, with explicit calls to
365Rather than having to insert ``m_app`` everywhere there is an
364Rather than having to insert ``m_app`` everywhere there is an
366application, we can use idiom brackets to do the job for us.
365application, 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``
368as follows, where ``<*>`` is defined in the same way as ``m_app``
367as follows, where ``<*>`` is defined in the same way as ``m_app``
369above (this is defined in the Idris library):
368above (this is defined in the Idris library):
371.. code-block:: idris
370.. code-block:: idris
373− instance Applicative Maybe where
372+ Applicative Maybe where
374 pure = Just
373 pure = Just
376 (Just f) <*> (Just a) = Just (f a)
375 (Just f) <*> (Just a) = Just (f a)
377 _ <*> _ = Nothing
376 _ <*> _ = Nothing
379−Using ``<*>`` we can use this instance as follows, where a function
378+Using ``<*>`` we can use this implementation as follows, where a function
380application ``[| f a1 …an |]`` is translated into ``pure f <*> a1 <*>
379application ``[| f a1 …an |]`` is translated into ``pure f <*> a1 <*>
381… <*> an``:
380… <*> an``:
@@ -407,8 +406,8 @@ We define a data type ``Eval`` to wrap an evaluator:
407 data Eval : Type -> Type where
406 data Eval : Type -> Type where
408 MkEval : (List (String, Int) -> Maybe a) -> Eval a
407 MkEval : (List (String, Int) -> Maybe a) -> Eval a
410−Wrapping the evaluator in a data type means we will be able to make it
409+Wrapping the evaluator in a data type means we will be able to provide
411−an instance of a type class later. We begin by defining a function to
410+implementations of interfaces for it later. We begin by defining a function to
412retrieve values from the context during evaluation:
411retrieve values from the context during evaluation:
414.. code-block:: idris
413.. code-block:: idris
@@ -421,18 +420,18 @@ retrieve values from the context during evaluation:
421 then (Just val)
420 then (Just val)
422 else (fetchVal xs)
421 else (fetchVal xs)
424−When defining an evaluator for the language, we will be applying
423+When defining an evaluator for the language, we will be applying functions in
425−functions in the context of an ``Eval``, so it is natural to make
424+the context of an ``Eval``, so it is natural to give ``Eval`` an implementation
426−``Eval`` an instance of ``Applicative``. Before ``Eval`` can be an
425+of ``Applicative``. Before ``Eval`` can have an implementation of
427−instance of ``Applicative`` it is necessary to make ``Eval`` an
426+``Applicative`` it is necessary for ``Eval`` to have an implementation of
428−instance of ``Functor``:
427+``Functor``:
430.. code-block:: idris
429.. code-block:: idris
432− instance Functor Eval where
431+ Functor Eval where
433 map f (MkEval g) = MkEval (\e => map f (g e))
432 map f (MkEval g) = MkEval (\e => map f (g e))
435− instance Applicative Eval where
434+ Applicative Eval where
436 pure x = MkEval (\e => Just x)
435 pure x = MkEval (\e => Just x)
438 (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
437 (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
@@ -454,24 +453,24 @@ to handle errors:
454 runEval env e = case eval e of
453 runEval env e = case eval e of
455 MkEval envFn => envFn env
454 MkEval envFn => envFn env
457−Named Instances
456+Named Implementations
458−===============
457+=====================
460−It can be desirable to have multiple instances of a type class, for
459+It can be desirable to have multiple implementations of an interface for the
461−example to provide alternative methods for sorting or printing values.
460+same type, for example to provide alternative methods for sorting or printing
462−To achieve this, instances can be *named* as follows:
461+values. To achieve this, implementations can be *named* as follows:
464.. code-block:: idris
463.. code-block:: idris
466− instance [myord] Ord Nat where
465+ [myord] Ord Nat where
467 compare Z (S n) = GT
466 compare Z (S n) = GT
468 compare (S n) Z = LT
467 compare (S n) Z = LT
469 compare Z Z = EQ
468 compare Z Z = EQ
470 compare (S x) (S y) = compare @{myord} x y
469 compare (S x) (S y) = compare @{myord} x y
472−This declares an instance as normal, but with an explicit name,
471+This declares an implementation as normal, but with an explicit name,
473−``myord``. The syntax ``compare @{myord}`` gives an explicit instance to
472+``myord``. The syntax ``compare @{myord}`` gives an explicit implementation to
474−``compare``, otherwise it would use the default instance for ``Nat``. We
473+``compare``, otherwise it would use the default implementation for ``Nat``. We
475can use this, for example, to sort a list of ``Nat`` in reverse.
474can use this, for example, to sort a list of ``Nat`` in reverse.
476Given the following list:
475Given the following list:
@@ -480,35 +479,34 @@ Given the following list:
480 testList : List Nat
479 testList : List Nat
481 testList = [3,4,1]
480 testList = [3,4,1]
483−We can sort it using the default ``Ord`` instance, then the named
482+We can sort it using the default ``Ord`` implementation, then the named
484−instance ``myord`` as follows, at the Idris prompt:
483+implementation ``myord`` as follows, at the Idris prompt:
488− *named_instance> show (sort testList)
487+ *named_impl> show (sort testList)
489 "[sO, sssO, ssssO]" : String
488 "[sO, sssO, ssssO]" : String
490− *named_instance> show (sort @{myord} testList)
489+ *named_impl> show (sort @{myord} testList)
491 "[ssssO, sssO, sO]" : String
490 "[ssssO, sssO, sO]" : String
494Determining Parameters
493Determining Parameters
495======================
494======================
497−When a class has more than one parameter, it can help resolution if
496+When an interface has more than one parameter, it can help resolution if the
498−the parameters used to resolve the type class are restricted. For
497+parameters used to find an implementation are restricted. For example:
501.. code-block:: idris
499.. code-block:: idris
503− class Monad m => MonadState s (m : Type -> Type) | m where
501+ interface Monad m => MonadState s (m : Type -> Type) | m where
504 get : m s
502 get : m s
505 put : s -> m ()
503 put : s -> m ()
507−In this class, only ``m`` needs to be known to resolve this class, and
505+In this interface, only ``m`` needs to be known to find an implementation of
508−``s`` can then be determined from the instance. This is declared with
506+this interface, and ``s`` can then be determined from the implementation. This
509−the ``| m`` after the class declaration. We call ``m`` a *determining
507+is declared with the ``| m`` after the interface declaration. We call ``m`` a
510−parameter* of the ``MonadState`` class, because it is the parameter
508+*determining parameter* of the ``MonadState`` interface, because it is the
511−used to resolve an instance.
509+parameter used to find an implementation.
514.. [1] Conor McBride and Ross Paterson. 2008. Applicative programming
512.. [1] Conor McBride and Ross Paterson. 2008. Applicative programming