[Haskell-cafe] Class Quantification

[Bas van Dijk]

On Wed, Oct 1, 2008 at 3:01 AM, Reiner Pope <reiner.pope at gmail.com> wrote:
> I believe there is no way to simply express this "abstraction over classes",
> but the Scrap your boilerplate with class[1] paper discusses this same
> problem and present a workaround by defining the class's dictionary of
> methods as an explicit type.
>
> What follows is the code to implement their workaround for your example.
>
> First some fairly standard extensions:
>
>> {-# LANGUAGE Rank2Types, EmptyDataDecls, FlexibleInstances, KindSignatures
>> #-}
>
> And some more controversial, but necessary ones:
>
>> {-# LANGUAGE UndecidableInstances, OverlappingInstances #-}
>>
>> module Cls where
>>
>
> The working bla function. Unfortunately, the "pseudoclass" cls needs
> to have its type explicitly named, hence the (uninhabited) Proxy type.
>
>> bla :: forall cls a c d. (Sat (cls c), Sat (cls d)) => Proxy cls ->
>> (forall b. Sat (cls b) => a -> b) -> a -> (c,d)
>> bla _ f x = (f x, f x)
>
> Again, testFoo and testBar unfortunately have to name which dictionary type
> to use, via the Proxy.
>
>> testFoo = bla (undefined :: Proxy NumD) fromInteger 1 :: (Int,Float)
>> testBar = bla (undefined :: Proxy ReadD) read "1" :: (Int,Float)
>
> The Sat class, straight from SYB:
>
>> class Sat a where
>>     dict :: a
>> data Proxy (cxt :: * -> *)
>
> The explicit dictionary construction for the Read class:
>
>> data ReadD a = ReadD { readsPrecD :: Int -> ReadS a }
>> instance (Read a) => Sat (ReadD a) where
>>     dict = ReadD readsPrec
>> instance (Sat (ReadD a)) => Read a where
>>     readsPrec = readsPrecD dict
>
> The explicit dictionary construction for the Num class:
>
>> data NumD a = NumD { plusD :: a -> a -> a,
>>                      timesD :: a -> a -> a,
>>                      negateD :: a -> a,
>>                      absD :: a -> a,
>>                      signumD :: a -> a,
>>                      fromIntegerD :: Integer -> a }
>> instance (Num a) => Sat (NumD a) where
>>     dict = NumD (+) (*) negate abs signum fromInteger
>
> We define these fake Eq,Show instances just to make the
> Num instance valid. It would be longer, but not more
> difficult, to genuinely encode the (Eq,Show)=>Num hierarchy.
>
>> instance (Sat (NumD a)) => Show a where {}
>> instance (Sat (NumD a)) => Eq a where {}
>> instance (Sat (NumD a)) => Num a where
>>     (+) = plusD dict
>>     (*) = timesD dict
>>     negate = negateD dict
>>     abs = absD dict
>>     signum = signumD dict
>>     fromInteger = fromIntegerD dict
>
> [1] http://homepages.cwi.nl/~ralf/syb3/ Sections 3.2 and 4.1
>
> On Wed, Oct 1, 2008 at 9:01 AM, Bas van Dijk <v.dijk.bas at gmail.com> wrote:
>>
>> On Tue, Sep 30, 2008 at 11:25 PM, Sean Leather <sean.leather at gmail.com>
>> wrote:
>> > But perhaps you're looking for potentially unknown classes?
>>
>> Yes indeed.
>>
>> Thanks,
>>
>> Bas
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>

Nice!

The explicit passing of the proxy type is indeed unfortunate but it's
nice that the type of your 'bla' is almost identical to mine:

> bla :: forall cls a c d. (Sat (cls c), Sat (cls d)) => Proxy cls -> (forall b. Sat (cls b) => a -> b) -> a -> (c,d)
> bla :: forall cls. (cls c, cls d) => (forall b. cls b => a -> b) -> a -> (c, d)

Thanks,

Bas