[Haskell-cafe] question about type constructors

[Roman Cheplyaka]

* TP <paratribulations at free.fr> [2013-05-23 13:23:36+0200]
> Roman Cheplyaka wrote:
> 
> > The rule of thumb is that you should never use IncoherentInstances.
> > 
> > The proper way to do it is:
> > 
> >   data Person :: Gender -> * where
> >       Person :: String -> Person b
> >       Child
> >         :: (PrettyPrint a, PrettyPrint b)
> >         => String -> Person a -> Person b -> Person c
> 
> Thanks a lot. Now I am using FlexibleContexts, and it works correctly (see 
> code below). I think I have understood the problem.
> However, I have still one question. In the code below, I have added data 
> constructors "Child2", "Child3" (imagining a world where every people has 
> three children). The problem is that I am compelled to repeat the context 
> "(PrettyPrint (Person a), PrettyPrint (Person b))" for each one of the 
> constructors. Is there any way to specify the context only once? I have 
> tried using "forall", but without any success.

No, because the type variables are independent across different
constructors.  They are (implicitly) existentially quantified, which
becomes clearer if you rewrite your type as

  data Person (c :: Gender)
    = forall a b . (PrettyPrint (Person a), PrettyPrint (Person b))
      => Child1 String (Person a) (Person b)
    | forall a b . (PrettyPrint (Person a), PrettyPrint (Person b))
      => Child2 String (Person a) (Person b)
    | ...

What you can do is factor out the Child type as

  data Child where
    Child :: ( PrettyPrint (Person a)
             , PrettyPrint (Person b)
             ) => String -> Person a -> Person b -> Child

  data Person a where
    Child1 :: Child -> Person c
    Child2 :: Child -> Person c
    Child3 :: Child -> Person c

> -------------
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE FlexibleInstances #-}
> {-# LANGUAGE FlexibleContexts #-}
> 
> class PrettyPrint a where
>     prettify :: a -> String
> 
> data Gender = Male | Female | Gender3 | Gender4
> 
> data Person :: Gender -> * where
>     Person :: String -> Person b
>     Child1 :: (PrettyPrint (Person a)
>              , PrettyPrint (Person b)
>              ) => String -> Person a -> Person b -> Person c
>     Child2 :: (PrettyPrint (Person a)
>              , PrettyPrint (Person b)
>              ) => String -> Person a -> Person b -> Person c
>     Child3 :: (PrettyPrint (Person a)
>              , PrettyPrint (Person b)
>              ) => String -> Person a -> Person b -> Person c
> 
> instance PrettyPrint (Person Male) where
>     prettify (Person name) = "My name is " ++ (show name)
>           ++ " and I am a male"
>     prettify (Child1 name person1 person2) = "My name is " ++ (show name)
>           ++ " and my parents are:" ++ (prettify person1) ++ ", "
>           ++ (prettify person2)
> 
> main = do
> 
> let a = Person "Jim" :: Person Male
> let b = Person "Joe" :: Person Male
> let c = Child1 "Jack" a b :: Person Male
> 
> print $ prettify a
> print $ prettify b
> print $ prettify c
> 
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe