RE: [Haskell] really undecidable instances?
This one can't. But it's hard to formulate a general rule. -fallow-undecidable-instances simply says that you, the programmer, take responsibility for termination. Without the flag, GHC uses a simple but sometimes over-conservative rule Simon | -----Original Message----- | From: haskell-bounces@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of Wolfgang | Jeltsch | Sent: 17 October 2005 14:17 | To: Haskell ML | Subject: [Haskell] really undecidable instances? | | Hello, | | what ist the problem with instance declarations like the following: | | instance C Int a => D Char [a] | | Why are such declarations only allowed with -fallow-undecidable-instances in | GHC? How can they result in undecidability? | | Best wishes, | Wolfgang | _______________________________________________ | Haskell mailing list | Haskell@haskell.org | http://www.haskell.org/mailman/listinfo/haskell
Am Montag, 17. Oktober 2005 15:57 schrieben Sie:
This one
[That is the instance declaration instance C Int a => D Char [a].]
can't. But it's hard to formulate a general rule. -fallow-undecidable-instances simply says that you, the programmer, take responsibility for termination. Without the flag, GHC uses a simple but sometimes over-conservative rule
Simon
[Could you please put citations at the top of the respective mail?] Section 7.4.4.3 of the GHC User's guide says about the restrictions for ensuring decidability: These restrictions ensure that context reduction terminates: each reduction step removes one type constructor. But as far as I can see, in my example there is also one type constructor removed. Why isn't this allowed then? Best wishes, Wolfgang
On Monday 17 October 2005 15:57, Simon Peyton-Jones wrote:
| Wolfgang Jeltsch: | what ist the problem with instance declarations like the following: | | instance C Int a => D Char [a] | | Why are such declarations only allowed with | -fallow-undecidable-instances in | GHC? How can they result in undecidability?
This one can't. But it's hard to formulate a general rule. -fallow-undecidable-instances simply says that you, the programmer, take responsibility for termination. Without the flag, GHC uses a simple but sometimes over-conservative rule
Hi, I've now been bitten by the same 'over-conservatism' of H98. In my case it's Non-type variables in constraint: Pretty (tree a) (Use -fallow-undecidable-instances to permit this) In the context: (Pretty a, Pretty (tree a)) This is the data type declaration:
data Node23 tree a = N2 (tree a) a (tree a) | N3 (tree a) a (tree a) a (tree a)
and this is the instance, where the error is reported:
instance (Pretty a, Pretty (tree a)) => Pretty (Node23 tree a) where ...
The class Pretty is from Daan Leijen's pprint library. I think that the 'non-type variable' refered to above is the application (tree a) in the constraint (Pretty (tree a)), which is arguably "almost" a type variable. In this case I think it is even more obvious that it can't cause a loop, since the LHS clearly has a type constructor removed, right? I mention this mainly because my module is otherwise completely H98 and I thought it would be nice to keep it that way. I need the Pretty instance for debugging only, so it's not really a show-stopper. Still I wonder if somebody knows a work-around that doesn't need a language extension (some newtype trick, maybe?). Ben
Benjamin Franksen writes:
This is the data type declaration:
data Node23 tree a = N2 (tree a) a (tree a) | N3 (tree a) a (tree a) a (tree a)
and this is the instance, where the error is reported:
instance (Pretty a, Pretty (tree a)) => Pretty (Node23 tree a) where ...
The class Pretty is from Daan Leijen's pprint library.
I think that the 'non-type variable' refered to above is the application (tree a) in the constraint (Pretty (tree a)), which is arguably "almost" a type variable. In this case I think it is even more obvious that it can't cause a loop, since the LHS clearly has a type constructor removed, right?
I mention this mainly because my module is otherwise completely H98 and I thought it would be nice to keep it that way. I need the Pretty instance for debugging only, so it's not really a show-stopper. Still I wonder if somebody knows a work-around that doesn't need a language extension (some newtype trick, maybe?).
I believe the "correct" way to do this is with a Pretty-promoting constructor class. class Pretty'1 f where pretty'1 :: Pretty a => f a -> Doc prettyList'1 :: Pretty a => [f a] -> Doc instance (Pretty a, Pretty'1 tree) => Pretty (Node23 tree a) where ... Your typical Pretty'1 instance will look like this: instance Pretty'1 T where pretty'1 = pretty prettyList'1 = prettyList -- David Menendez <zednenem@psualum.com> | "In this house, we obey the laws <http://www.eyrie.org/~zednenem> | of thermodynamics!"
On Sunday 30 October 2005 21:59, David Menendez wrote:
Benjamin Franksen writes:
This is the data type declaration:
data Node23 tree a = N2 (tree a) a (tree a)
| N3 (tree a) a (tree a) a (tree a)
and this is the instance, where the error is reported:
instance (Pretty a, Pretty (tree a)) => Pretty (Node23 tree a) where ...
The class Pretty is from Daan Leijen's pprint library.
I think that the 'non-type variable' refered to above is the application (tree a) in the constraint (Pretty (tree a)), which is arguably "almost" a type variable. In this case I think it is even more obvious that it can't cause a loop, since the LHS clearly has a type constructor removed, right?
I mention this mainly because my module is otherwise completely H98 and I thought it would be nice to keep it that way. I need the Pretty instance for debugging only, so it's not really a show-stopper. Still I wonder if somebody knows a work-around that doesn't need a language extension (some newtype trick, maybe?).
I believe the "correct" way to do this is with a Pretty-promoting constructor class.
class Pretty'1 f where pretty'1 :: Pretty a => f a -> Doc prettyList'1 :: Pretty a => [f a] -> Doc
instance (Pretty a, Pretty'1 tree) => Pretty (Node23 tree a) where ...
Your typical Pretty'1 instance will look like this:
instance Pretty'1 T where pretty'1 = pretty prettyList'1 = prettyList
Works like a charm. Thanks a lot! Ben
participants (4)
-
Benjamin Franksen -
David Menendez -
Simon Peyton-Jones -
Wolfgang Jeltsch