Edward Kmett - Type Classes vs. the World

By: Boston Haskell

164   1   17215

Uploaded on 02/16/2015

Boston Haskell Meetup - January 21, 2015

Comments (7):

By anonymous    2017-09-20

I wrote a long answer about Hasochism's Matrix's Applicative instance, using finite sets as index types, but it's probably overkill for what you wanted, not to mention less efficient than the Array-based code in the blog post.

Your problem stems from the fact that various operations in the blog post's code assume that the Bounded instance for the matrix's index type is covering, in the sense that every value within the bounds will have a corresponding element in the matrix. The core assumption seems to be that the size of the matrix is known statically.

The simplest way to fix this would be to make an adjustment to the Matrix type, so that it carries its size around with it. You still have to do all your bounds checking dynamically, but I think that's a fairly good trade-off compared to the weightiness of the Hasochism approach.

-- Bounded as an explicit (minBound, maxBound) tuple
type Bounds i = (i, i)
data Matrix i e = Matrix { getBounds :: Bounds i, getMatrix :: Array (Edge i) e }

entireRange :: Ix i => Bounds i -> [i]
entireRange b = range b

matrix :: Ix i => Bounds i -> (Edge i -> e) -> Matrix i e
matrix bounds f = Matrix bounds $ listArray bounds $ map f $ entireRange bounds

This gets stuck, however, when you need to construct a matrix in a type class instance. You can't abstract instances over runtime values: the only thing valid to the left of the => in an instance declaration is another type class constraint. In a declaration like

instance Bounded i => Applicative (Matrix i) where
    pure x = matrix (const x)
    (<*>) = -- ...

we have no choice than to pass the bounds statically in an instance dictionary because the type of pure doesn't allow us to pass explicit configuration data. This restriction has its ups and downs, but right now it's a definite downer: the fix is to rip all of the classiness out of your code altogether.

Good news, though: you can emulate this explicit dictionary-passing style using the crazy reflection library, which does evil, magical things to push runtime values into typeclass dictionaries. It's scary stuff, but it does work, and it's safe.

It all happens in the reify and reflect combinators. reify takes a runtime value and a block of code with a constraint depending on the availability of that value and plugs them in to one another. Calls to reflect inside the block return the value that was passed to reify outside it.

needsAnInt :: Reifies s Int => Proxy s -> IO ()
needsAnInt p = print (reflect p + 1)

example1 :: IO ()
example1 = reify 3 (\p -> needsAnInt p)  -- prints 4
example2 :: IO ()
example2 = reify 5 (\p -> needsAnInt p)  -- prints 6

Take a moment to reflect (ha ha) on how weird this is. Usually there's only one class dictionary in scope for each type (overlapping instances notwithstanding). Proxy has only one value (data Proxy a = Proxy), so how can reflect tell two proxies apart, to return different values each time?

Anyway, what's the point of this? Instances can't depend on runtime values, but they can depend on other instances. reflection gives us the tools to turn a runtime value into an instance dictionary, so this allows us to build instances which depend dynamically on runtime values!

In this case, we're building an instance of Bounded. We need a newtype, to make an instance which doesn't overlap with any others:

-- in this case it's fine to just lift the Ix instance from the underlying type
newtype B s i = B i deriving (Eq, Ord, Ix)

Clearly B can be an instance of Bounded if i is - it can get minBound and maxBound from i's instance - but we want to get them from a Reifies context. In other words, the runtime value we'll be stuffing into the Reifies dictionary will be a pair of is.

instance Reifies s (i, i) => Bounded (B s i) where
    minBound = B $ fst $ reflect (Proxy :: Proxy s)
    maxBound = B $ snd $ reflect (Proxy :: Proxy s)

I'm using ScopedTypeVariables crucially to come up with Proxy values of the correct type.

Now you can write perfectly ordinary code which uses a Bounded context (even if that context arises due to some other instance), and invoke it with a dynamically built Bounded dictionary using reify.

entireRange :: (Ix i, Bounded i) => [i]
entireRange = range (minBound, maxBound)

example3 :: IO ()
example3 = reify (3, 6) myComputation
    where myComputation :: forall s. Bounded (B s Int) => Proxy s -> IO ()
          myComputation p = print $ map unB (entireRange :: [B s Int])

ghci> example3

Um, yeah. reflection can be tricky to use. At the end of the day, it's probably simpler just to not bother with classes.

Original Thread

By anonymous    2017-09-20

The constraints package provides a solution to this problem, via its :- ("entails") type:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

import GHC.Exts

data Dict :: Constraint -> * where
    Dict :: a => Dict a

newtype a :- b = Sub (a => Dict b)
infixr 9 :-

g, g' :: c2 a => c2 a :- c1 a -> (forall b. c1 b => b) -> a
g (Sub Dict) x = x

Then, by passing in an appropriate witness, we can recover the original example:

integralImpliesNum :: Integral a :- Num a
integralImpliesNum = Sub Dict

f :: Integral a => (forall b. Num b => b) -> a
f = g integralImpliesNum

In fact, this g is merely a flipped and specialized version of the \\ operator:

(\\) :: a => (b => r) -> (a :- b) -> r
r \\ Sub Dict = r
infixl 1 \\

g' = flip (\\)

If you have the time, Edward Kmett's talk "Type Classes vs the World" is a great introduction to how this all works.

Original Thread

By anonymous    2017-09-20

In a comment I made an assertion without justifying myself: I said that return type polymorphism isn't a meaningful concept in an untyped language. That was rude of me and I apologise for being so brusque. What I meant was something rather more subtle than what I said, so please allow me to attempt to make amends for my poor communication by explaining in more detail what I was trying to get at. (I hope this answer doesn't come across as condescending; I don't know your base level of knowledge so I'm going to start at the beginning.)

When Haskellers say "return type polymorphism", they're referring to one particular effect of the type class dispatch mechanism. It comes about as the interplay between dictionary passing and bidirectional type inference. (I'm going to ignore polymorphic _|_s like undefined :: forall a. a or let x = x in x :: forall a. a. They don't really count.)

First, note that type class instances in Haskell are syntactic sugar for explicit dictionary passing. By the time GHC translates your program into its Core intermediate representation, all the type classes are gone. They are replaced with "dictionary" records and passed around as regular explicit arguments; => is represented at runtime as ->. So code like

class Eq a where
    (==) :: a -> a -> Bool
instance Eq Bool where
    True == True = True
    False == False = True
    _ == _ = False

headEq :: Eq a => a -> [a] -> Bool
headEq _ [] = False
headEq x (y:_) = x == y

main = print $ headEq True [False]

is translated into something like

-- The class declaration is translated into a regular record type. (D for Dictionary)
data EqD a = EqD { eq :: a -> a -> Bool }
-- The instance is translated into a top-level value of that type
eqDBool :: EqD Bool
eqDBool = EqD { eq = eq }
    where eq True True = True
          eq False False = True
          eq _ _ = False

-- the Eq constraint is translated into a regular dictionary argument
headEq :: EqD a -> a -> [a] -> Bool
headEq _ _ [] = False
headEq eqD x (y:_) = eq eqD x y

-- the elaborator sees you're calling headEq with a ~ Bool and passes in Bool's instance dictionary
main = print $ headEq eqDBool True [False]

It works because of instance coherence: every constraint has at most one "best" matching instance (unless you switch on IncoherentInstances, which is usually a bad idea). At the call site of an overloaded function, the elaborator looks at the constraint's type parameter, searches for an instance matching that constraint - either a top-level instance or a constraint that's in scope - and passes in the single corresponding dictionary as an argument. (For more on the notion of instance coherence I recommend this talk by Ed Kmett. It's quite advanced - it took me a couple of watches to grasp his point - but it's full of insight.)

Much of the time, as in headEq, the constraint's type parameters can be determined by looking only at the types of the overloaded function's arguments, but in the case of polymorphic return values (such as read :: Read a => String -> a or mempty :: Monoid m => m) the typing information has to come from the call site's context. This works via the usual mechanism of bidirectional type inference: GHC looks at the return value's usages, generates and solves unification constraints to figure out its type, and then uses that type to search for an instance. It makes for a kinda magical developer experience: you write mempty and the machine figures out from the context which mempty you meant!

(Incidentally, that's why show . read :: String -> String is forbidden. show and read are type class methods, whose concrete implementation isn't known without any clues about the type at which they're being used. The intermediate type in show . read - the one you're reading into and then showing from - is ambiguous, so GHC doesn't know how to choose an instance dictionary in order to generate runtime code.)

So "return type polymorphism" is actually a slightly misleading term. It's really a by-word for a particular kind of type-directed code generation; its Core representation is just as a regular function whose return type can be determined from the type of its (dictionary) argument. In a language without type classes (or a language without types at all, like JS), you have to simulate type classes with explicit dictionary parameters that are manually passed around by the programmer, as @4Castle has demonstrated in another answer. You can't do type-directed code generation without types to be directed by!

Original Thread

By anonymous    2017-12-04

You just invented type classes! A class is a dictionary of functions. During compilation, code like

class Monoid a where
    mempty :: a
    mappend :: a -> a -> a

instance Monoid [a] where
    mempty = []
    mappend = (++)

mconcat :: Monoid a => [a] -> a
mconcat = foldr mappend

main = print $ mconcat ["foo", "bar"]

is translated into explicit dictionary-passing style.

data Monoid a = Monoid { mempty :: a, mappend :: a -> a -> a }

list_monoid = Monoid [] (++)

mconcat :: Monoid a -> [a] -> a
mconcat monoid = foldr (mappend monoid)

main = print $ mconcat list_monoid ["foo", "bar"]

That translation is exactly the most important difference between type classes and dictionaries: classes are implicit. You don't have to explicitly pass the monoid variable around - the compiler takes care of the plumbing for you. It would be especially tedious to build composed instances like Ord a => Ord [a] by hand.

There's one other key difference between classes and dictionaries, and that's coherence. Basically, there's always at most one "best" instance to satisfy a given constraint, that instance is global and unique, and you can't override it. With dictionary-passing style, on the other hand, the function will just use whatever dictionary you passed in and there are no guarantees of uniqueness. This is sometimes good and sometimes bad.

Original Thread

Recommended Books

    Submit Your Video

    If you have some great dev videos to share, please fill out this form.