Hi, In the program I am trying to write, I have a problem that can be reduced to the following dummy example: -------------------------- {-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE IncoherentInstances #-} class PrettyPrint a where prettify :: a -> String data Gender = Male | Female | Gender3 | Gender4 data Person :: Gender -> * where Person :: String -> Person b Child :: String -> Person a -> Person b -> Person c instance PrettyPrint (Person a) instance PrettyPrint (Person Male) where prettify (Person name) = "My name is " ++ (show name) ++ " and I am a male" prettify (Child name person1 person2) = "My name is " ++ (show name) ++ " and my parents are:" ++ (prettify person1) ++ ", " ++ (prettify person2) main = do let p1 = Person "Jim" :: Person Male let p2 = Person "Joe" :: Person Male let p3 = Child "Jack" p1 p2 print $ prettify p1 print $ prettify p2 print $ prettify p3 -------------------------- The idea is that I want to implement PrettyPrint only for a subset of the possible types in Gender (through promotion process). Why? It would be longer to explain (it is a bit more complicated in my real program). Anyway, in the program above, I have found that with IncoherentInstances (and the empty instance definition for (Person a)), it is working, it is able to use the most specific instance corresponding to the current type (I don't know exactly why). For example, p1 and p2 are correctly printed above, because they are of type (Person Male) and because I have implemented PrettyPrint for (Person Male). But it does not work for p3, I obtain an error at runtime: ----- $ runghc test.hs "My name is \"Jim\" and I am a male" "My name is \"Joe\" and I am a male" test_typelost.hs: test_typelost.hs:16:10-31: No instance nor default method for class operation Main.prettify ----- The reason is that the information that p1 and p2 are Male seems to be "lost" when we construct the child "Child "Jack" p1 p2", probably because GHC only sees that in the type signature of Child, we have a more general (Person a) -> (Person b). So he tries to find an implementation of prettify in PrettyPrint (Person a), but there is none. Is there any workaround? Thanks, TP
* TP
Hi,
In the program I am trying to write, I have a problem that can be reduced to the following dummy example:
-------------------------- {-# LANGUAGE GADTs #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE IncoherentInstances #-}
class PrettyPrint a where prettify :: a -> String
data Gender = Male | Female | Gender3 | Gender4
data Person :: Gender -> * where Person :: String -> Person b Child :: String -> Person a -> Person b -> Person c
instance PrettyPrint (Person a)
instance PrettyPrint (Person Male) where prettify (Person name) = "My name is " ++ (show name) ++ " and I am a male" prettify (Child name person1 person2) = "My name is " ++ (show name) ++ " and my parents are:" ++ (prettify person1) ++ ", " ++ (prettify person2)
main = do
let p1 = Person "Jim" :: Person Male let p2 = Person "Joe" :: Person Male let p3 = Child "Jack" p1 p2
print $ prettify p1 print $ prettify p2 print $ prettify p3 --------------------------
The idea is that I want to implement PrettyPrint only for a subset of the possible types in Gender (through promotion process). Why? It would be longer to explain (it is a bit more complicated in my real program).
Anyway, in the program above, I have found that with IncoherentInstances (and the empty instance definition for (Person a)), it is working, it is able to use the most specific instance corresponding to the current type (I don't know exactly why). For example, p1 and p2 are correctly printed above, because they are of type (Person Male) and because I have implemented PrettyPrint for (Person Male).
But it does not work for p3, I obtain an error at runtime: ----- $ runghc test.hs "My name is \"Jim\" and I am a male" "My name is \"Joe\" and I am a male" test_typelost.hs: test_typelost.hs:16:10-31: No instance nor default method for class operation Main.prettify -----
The reason is that the information that p1 and p2 are Male seems to be "lost" when we construct the child "Child "Jack" p1 p2", probably because GHC only sees that in the type signature of Child, we have a more general (Person a) -> (Person b). So he tries to find an implementation of prettify in PrettyPrint (Person a), but there is none.
Is there any workaround?
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 Roman
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. Thanks, TP ------------- {-# 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
* TP
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (2)
-
Roman Cheplyaka -
TP