Re: [Haskell-cafe] rip in the class-abstraction continuum

2013-05-21 Thread oleg

Type classes are the approach to constrain type variables, to bound
polymorphism and limit the set of types the variables can be
instantiated with. If we have two type variables to constrain,
multi-parameter type classes are the natural answer then. Let's take
this solution and see where it leads to.

Here is the original type class
 class XyConv a where
   toXy :: a b - [Xy b]

and the problematic instance
 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

To be more explicit, the type class declaration has the form

 class XyConv a where
   toXy :: forall b. a b - [Xy b]

with the type variable 'b' universally quantified without any
constraints. That means the user of (toXy x) is free to choose any type
for 'b' whatsoever. Obviously that can't be true for 
(toXy (CircAppr x y)) since we can't instantiate pi to any type. It
has to be a Floating type. Hence we have to constrain b. As I said, the
obvious solution is to make it a parameter of the type class.

We get the first solution:

 class XYConv1 a b where
 toXy1 :: a b - [Xy b]

 instance (Floating b, Integral a) = XYConv1 (CircAppr a) b where
   toXy1 (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

The type class declaration proclaims that only certain combinations of
'a' and 'b' are admitted to the class XYConv1. In particular, 'a' is
(CircAppr a) and 'b' is Floating. 

This reminds us of collections (with Int keys, for simplicity)

 class Coll c where
   empty :: c b
   insert :: Int - b - c b - c b

 instance Coll M.IntMap where
   empty  = M.empty
   insert = M.insert

The Coll declaration assumes that a collection is suitable for elements of
any type. Later on one notices that if elements are Bools,
they can be stuffed quite efficiently into an Integer. If we wish to
add ad hoc, efficient collections to the framework, we have to
restrict the element type as well:

 class Coll1 c b where
   empty1 :: c
   insert1 :: Int - b - c - c

Coll1 is deficient since there is no way to specify the type
of elements for the empty collection. When the type checker sees
'empty1', how can it figure out which instance for Coll1 (with the
same c but different element types) to choose?
We can help the type-checker by declaring (by adding the functional
dependency c - b) that for each collection
type c, there can be only one instance of Coll1. In other words, the
collection type determines the element type.

Exactly the same principle works for XYConv.

 class XYConv2 a b | a - b where
 toXy2 :: a - [Xy b]

 instance (Floating b, Integral a) = XYConv2 (CircAppr a b) b where
   toXy2 (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

The third step is to move to associated types. At this stage you can
consider them just as a different syntax of writing functional
dependencies:

 class XYConv3 a where
 type XYT a :: *
 toXy3 :: a - [Xy (XYT a)]

 instance (Floating b, Integral a) = XYConv3 (CircAppr a b) where
   type XYT (CircAppr a b) = b
   toXy3 (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

The step from XYConv2 to XYConv3 is mechanical. The class XYConv3
assumes that for each convertible 'a' there is one and only Xy type
'b' to which it can be converted. This was the case for (CircAppr a
b). It may not be the case in general. But we can say that for each
convertible 'a' there is a _class_ of Xy types 'b' to which they may be
converted. This final step brings Tillmann Rendel's solution.



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] rip in the class-abstraction continuum

2013-05-20 Thread Tillmann Rendel

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

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] rip in the class-abstraction continuum

2013-05-20 Thread Christopher Howard
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



signature.asc
Description: OpenPGP digital signature
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe