rip in the class-abstraction continuum

Hi. I won't pretend to be an advanced Haskell programmer. However, I have a strong interest in abstraction, and I have been playing around with programming as abstractly as possible. Naturally, I find classes to be quite attractive and useful. However, something is bothering me. Lately I keep running into this situation where I have to cut across abstraction layers in order to make the code work. More specifically, I keep finding that I have to add constraints to a class definition, because eventually I find some instance of that class which needs those constraints to compile. For example, I wanted to create a class which represents all things that can be converted into X,Y coordinates. Naturally, I would like to do something like this: code: -------- class XyConv a where toXy :: a b -> [Xy b] -------- This leaves me free in the future to use any number type conceivable in the Xy coordinates - Floating or Integral types, or whatever. (Doesn't even have to be numbers, actually!) However the first instance I create, requires me to use operators in the function definition which require at least a Floating type. (The error will say Fractional, but there are other components that also require Floating.) code: -------- data CircAppr a b = CircAppr a b b -- number of points, rotation angle, radius deriving (Show) instance Integral a => XyConv (CircAppr a) where toXy (CircAppr divns ang rad) = let dAng = 2 * pi / (fromIntegral divns) in let angles = map ((+ ang) . (* dAng) . fromIntegral) [0..divns] in map (\a -> am2xy a rad) angles -------- This gives me the error code: -------- Could not deduce (Fractional b) arising from a use of `/' from the context (Integral a) bound by the instance declaration at /scratch/cmhoward/pulse-spin/pulse-spin.hs:51:10-42 Possible fix: add (Fractional b) to the context of the type signature for toXy :: CircAppr a b -> [Xy b] or the instance declaration In the expression: 2 * pi / (fromIntegral divns) In an equation for `dAng': dAng = 2 * pi / (fromIntegral divns) In the expression: let dAng = 2 * pi / (fromIntegral divns) in let angles = map ((+ ang) . (* dAng) . fromIntegral) [0 .. divns] in map (\ a -> am2xy a rad) angles -------- I can get a quick fix by adding Floating to the context of the /class/ definition: code: -------- class XyConv a where toXy :: Floating b => a b -> [Xy b] -------- But what I really want is to put Floating in the context of the /instance/ declaration. But I don't know how to do that syntactically. -- frigidcode.com

Hi, Christopher Howard wrote:
class XyConv a where toXy :: a b -> [Xy b]
[...]
I can get a quick fix by adding Floating to the context of the /class/ definition:
class XyConv a where toXy :: Floating b => a b -> [Xy b]
But what I really want is to put Floating in the context of the /instance/ declaration.
This is not easily possible. If you could just put the constraint into the instance, there would be a problem when youc all toXy in a polymorphic context, where a is not known. Example: class XyConv a where toXy :: a b -> [Xy b] shouldBeFine :: XyConv a => a String -> [Xy String] shouldBeFine = toXy This code compiles fine, because the type of shouldBeFine is an instance of the type of toXy. The type checker figures out that here, b needs to be String, and since there is no class constraint visible anywhere that suggests a problem with b = String, the code is accepted. The correctness of this reasoning relies on the fact that whatever instances you add in other parts of your program, they can never constrain b so that it cannot be String anymore. Such an instance would invalidate the above program, but that would be unfair: How would the type checker have known in advance whether or not you'll eventually write this constraining instance. So this is why in Haskell, the type of a method in an instance declaration has to be as general as the declared type of that method in the corresponding class declaration. Now, there is a way out using some of the more recent additions to the language: You can declare, in the class, that each instance can choose its own constraints for b. This is possible by combining constraint kinds and associated type families. {-# LANGUAGE ConstraintKinds, TypeFamilies #-} import GHC.Exts The idea is to add a constraint type to the class declaration: class XyConv a where type C a :: * -> Constraint toXy :: C a b => a b -> [Xy b] Now it is clear to the type checker that calling toXy requires that b satisfies a constraint that is only known when a is known, so the following is not accepted. noLongerAccepted :: XyConv a => a String -> [Xy String] noLongerAccepted = toXy The type checker complains that it cannot deduce an instance of (C a [Char]) from (XyConv a). If you want to write this function, you have to explicitly state that the caller has to provide the (C a String) instance, whatever (C a) will be: haveToWriteThis :: (XyConv a, C a String) => a String -> [Xy String] haveToWriteThis = toXy So with associated type families and constraint kinds, the class declaration can explicitly say that instances can require constraints. The type checker will then be aware of it, and require appropriate instances of as-yet-unknown classes to be available. I think this is extremely cool and powerful, but maybe more often than not, we don't actually need this power, and can provide a less generic but much simpler API. Tillmann

On 05/19/2013 10:10 PM, Tillmann Rendel wrote:
This is not easily possible. If you could just put the constraint into the instance, there would be a problem when youc all toXy in a polymorphic context, where a is not known. Example:
class XyConv a where toXy :: a b -> [Xy b]
shouldBeFine :: XyConv a => a String -> [Xy String] shouldBeFine = toXy
This code compiles fine, because the type of shouldBeFine is an instance of the type of toXy. The type checker figures out that here, b needs to be String, and since there is no class constraint visible anywhere that suggests a problem with b = String, the code is accepted.
The correctness of this reasoning relies on the fact that whatever instances you add in other parts of your program, they can never constrain b so that it cannot be String anymore. Such an instance would invalidate the above program, but that would be unfair: How would the type checker have known in advance whether or not you'll eventually write this constraining instance.
So this is why in Haskell, the type of a method in an instance declaration has to be as general as the declared type of that method in the corresponding class declaration.
Now, there is a way out using some of the more recent additions to the language: You can declare, in the class, that each instance can choose its own constraints for b. This is possible by combining constraint kinds and associated type families.
{-# LANGUAGE ConstraintKinds, TypeFamilies #-} import GHC.Exts
The idea is to add a constraint type to the class declaration:
class XyConv a where type C a :: * -> Constraint toXy :: C a b => a b -> [Xy b]
Now it is clear to the type checker that calling toXy requires that b satisfies a constraint that is only known when a is known, so the following is not accepted.
noLongerAccepted :: XyConv a => a String -> [Xy String] noLongerAccepted = toXy
The type checker complains that it cannot deduce an instance of (C a [Char]) from (XyConv a). If you want to write this function, you have to explicitly state that the caller has to provide the (C a String) instance, whatever (C a) will be:
haveToWriteThis :: (XyConv a, C a String) => a String -> [Xy String] haveToWriteThis = toXy
So with associated type families and constraint kinds, the class declaration can explicitly say that instances can require constraints. The type checker will then be aware of it, and require appropriate instances of as-yet-unknown classes to be available. I think this is extremely cool and powerful, but maybe more often than not, we don't actually need this power, and can provide a less generic but much simpler API.
Tillmann
Thank you for the quick and thorough response. To be honest though, I had some difficulty following your explanation of the constraints problem. I had an even more difficult time when I tried to read up on what Type Families are -- ended up at some wiki page trying to explain Type Families by illustrating them with Generic Finite Maps (a.k.a., Generic Prefix Trees). The rough equivalent of learning German through a Latin-German dictionary. :| Anyway, I played around with my code some more - and it seems like what I am trying to do can be done with multi-parameter type classes: code: -------- {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-} class XyConv a b where toXy :: a b -> [Xy b] instance (Integral a, Floating b) => XyConv (CircAppr a) b where toXy (CircAppr divns ang rad) = let dAng = 2 * pi / (fromIntegral divns) in let angles = map ((+ ang) . (* dAng) . fromIntegral) [0..divns] in map (\a -> am2xy a rad) angles -------- Seems to work okay: code: -------- h> toXy (CircAppr 4 0.0 1.0) [Xy 1.0 0.0,Xy 6.123233995736766e-17 1.0,Xy (-1.0) 1.2246467991473532e-16,Xy (-1.8369701987210297e-16) (-1.0),Xy 1.0 (-2.4492935982947064e-16)] h> :t toXy (CircAppr 4 0.0 1.0) toXy (CircAppr 4 0.0 1.0) :: Floating b => [Xy b] -------- Is there anything bad about this approach? -- frigidcode.com
participants (2)
-
Christopher Howard
-
Tillmann Rendel