[Haskell-beginners] Fwd: Type constraints question

[Daniel Fischer]

Am Samstag 19 Dezember 2009 00:55:34 schrieb David Gordon:
> Apologies for the spam, I had some difficulty getting my email address set
> up right on the list and wanted to make sure this finally got through (or
> perhaps there are like 5 copies on the list now... sorry.)
>
> thanks
>
> ---------- Forwarded message ----------
>
> Ok, now I will try asking the right question (previous try wasn't actually
> an example of the problem I'm having)
>
> Here's the code:
>
>
> data Test = Test
>
> data Test2 = Test2
>
> class MyClass a where
>     getChild :: MyClass b => a -> b
>
> instance MyClass Test where
>     getChild a = Test2
>
> instance MyClass Test2 where
>     getChild a = Test
>
> On HUGS I get:
>
> Error occurred
> ERROR line 9 - Inferred type is not general enough
> *** Expression    : getChild
> *** Expected type : (MyClass Test, MyClass a) => Test -> a
> *** Inferred type : (MyClass Test, MyClass Test2) => Test -> Test2
>
> So, what's the problem with always returning a particular instance of
> MyClass? I just want to constrain it to be an instance of MyClass, nothing
> more.

The signature of getChild promises that *whichever type the caller wants*, as long as it's 
a member of MyClass, it can be provided. The implementation returns one specific type.

It's different from interfaces in Java, where the callee decides which type is returned, 
here the caller can demand the type that the callee has to return.

The signature of getChild is actually

getChild :: forall b. MyClass b => a -> b

while the implementation has the signature (not legal Haskell)

getChild :: exists b. MyClass b => a -> b.

What you want is, I believe, that each instance a of MyClass specifies a type b belonging 
to MyClass which getChild returns.
You can achieve part of that for example with a multiparameter type class

{-# LANGUAGE MultiParamTypeClasses #-}

class MyClass2 a b where
    getChild :: a -> b

However, this allows that a has children of more than one type (

instance MyClass2 Test Test2 where
    getChild _ = Test2

instance MyClass2 Test Test where
    getChild _ = Test

) and this doesn't enforce that b itself has children.

To enforce that every type has only one type of children, you can use functional 
dependencies (or type families, see below):

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}

class MyClass3 a b | a -> b where
    getChild :: a -> b

The functional dependency "a -> b" (separated from the class head by "|") says that a 
uniquely determines b. But that still doesn't enforce that b has children. For that, you 
need

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts #-}

class MyClass4 a b | a -> b where
    getChild :: MyClass4 b c => a -> b

Now each type can have only one type of children and they must have children too.

Another way to achieve the above is via type families:

{-# LANGUAGE TypeFamilies, FlexibleContexts #-}

class MyClass5 a where
    type Child a :: *
    getChild :: (MyClass5 (Child a)) => a -> Child a

instance MyClass5 Test where
    type Child Test = Test2
    getChild _ = Test2

instance MyClass5 Test2 where
    type Child Test2 = Test
    getChild _ = Test



>
> thanks,
>
> David
>
>
> 2009/12/18 David Gordon <david.robert.gordon at googlemail.com>
>
> > Hi Folks,
> > Total newbie here. I don't know if I am having a syntactic problem or a
>
> conceptual problem.
>
> > This code:
> > data Test = Test
> > data Test2 = Test2
> > class MyClass a where
> >     getChild :: (MyClass b) => a -> b
> > instance MyClass Test where
> >     getChild = Test2
> > instance MyClass Test2 where
> >     getChild = Test
> > results in:
> > [1 of 1] Compiling Main             ( test.hs, interpreted )
> > test.hs:10:15:
> >     Couldn't match expected type `Test -> b'
> >            against inferred type `Test2'
> >     In the expression: Test2
> >     In the definition of `getChild': getChild = Test2
> >     In the instance declaration for `MyClass Test'
> > test.hs:13:15:
> >     Couldn't match expected type `Test2 -> b'
> >            against inferred type `Test'
> >     In the expression: Test
> >     In the definition of `getChild': getChild = Test
> >     In the instance declaration for `MyClass Test2'
> > Failed, modules loaded: none.
> > Is this a reasonable thing to try and do in Haskell? If not, I have a lot
>
> more questions... ;)
>
> > many thanks,
> > David