Hello all! Consider the following program:
{-# LANGUAGE FlexibleInstances, OverlappingInstances, UndecidableInstances #-}
class B a => A a
instance A Int
class Eq a => B a
instance (A a, Eq a) => B a
eq :: B a => a -> a -> Bool eq = (==)
test = 1 `eq` (2::Int)
(This is a condensed version of a much larger program that I've been debugging.) It compiles just fine, but `test` doesn't terminate (GHCi 6.10.4). If I change the context `B a` to `Eq a` for the function `eq`, it terminates. Although I don't know all the details of the class system, it seems unintuitive that I can make a program non-terminating just by changing the context of a function (regardless of UndecidableInstances etc.). Is this a bug or a feature? / Emil
On Fri, Jan 22, 2010 at 12:24:37PM +0100, Emil Axelsson wrote:
Consider the following program:
{-# LANGUAGE FlexibleInstances, OverlappingInstances, UndecidableInstances #-} class B a => A a
instance A Int
class Eq a => B a
instance (A a, Eq a) => B a [...] Although I don't know all the details of the class system, it seems unintuitive that I can make a program non-terminating just by changing the context of a function (regardless of UndecidableInstances etc.).
Is this a bug or a feature?
I'm afraid you voided the warranty when you used UndecidableInstances. You really do have a circularity between A and B here, so it's not surprising that you get a loop. By changing the context, you demanded more instances, undecidable ones in fact.
Ross Paterson skrev:
On Fri, Jan 22, 2010 at 12:24:37PM +0100, Emil Axelsson wrote:
Consider the following program:
{-# LANGUAGE FlexibleInstances, OverlappingInstances, UndecidableInstances #-} class B a => A a
instance A Int
class Eq a => B a
instance (A a, Eq a) => B a [...] Although I don't know all the details of the class system, it seems unintuitive that I can make a program non-terminating just by changing the context of a function (regardless of UndecidableInstances etc.).
Is this a bug or a feature?
I'm afraid you voided the warranty when you used UndecidableInstances.
You really do have a circularity between A and B here, so it's not surprising that you get a loop. By changing the context, you demanded more instances, undecidable ones in fact.
But still, I've always heard that "undecidable instances can cause the type checker to loop, but if the compiler terminates, you're fine". Here the loop happens at run time, so undecidable instances must be a little more evil than I thought... / Emil
It's a feature! You have * B is a superclass of A * Eq is a superclass of B So every A dictionary has a B dictionary inside it, and every B dictionary has an Eq dictionary inside it. Now, your instance declaration instance (A a, Eq a) => B a says "if you give me an A dictionary and an Eq dictionary, I'll make you a B dictionary". Now, 'test' needs a (B Int) dictionary. To get one, we need an (A Int) dictionary and an (Eq Int) dictionary. But when solving these sub-problems, GHC assumes that you have in hand a solution to the original problem, this case (B Int) Why? Read the SYB3 paper. OK so now you see the problem: we can solve the (A Int) and (Eq Int) sub-problems by selection from the (B Int) dictionary. Still, I confess that I have not fully grokked the relationship between the SYB3-style recursion stuff and the question of superclasses. So I will think about your example some more, thank you. Meanwhile, it's clear that you are on thin ice. Simon | -----Original Message----- | From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe-bounces@haskell.org] On | Behalf Of Emil Axelsson | Sent: 22 January 2010 11:25 | To: Haskell Cafe | Subject: [Haskell-cafe] Non-termination due to context | | Hello all! | | Consider the following program: | | > {-# LANGUAGE FlexibleInstances, OverlappingInstances, UndecidableInstances #-} | > | > class B a => A a | > | > instance A Int | > | > class Eq a => B a | > | > instance (A a, Eq a) => B a | > | > eq :: B a => a -> a -> Bool | > eq = (==) | > | > test = 1 `eq` (2::Int) | | (This is a condensed version of a much larger program that I've been | debugging.) | | It compiles just fine, but `test` doesn't terminate (GHCi 6.10.4). If I | change the context `B a` to `Eq a` for the function `eq`, it terminates. | | Although I don't know all the details of the class system, it seems | unintuitive that I can make a program non-terminating just by changing | the context of a function (regardless of UndecidableInstances etc.). | | Is this a bug or a feature? | | / Emil | | _______________________________________________ | Haskell-Cafe mailing list | Haskell-Cafe@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe
OK, I'll try to get to the SYB3 paper at some point. For now I'll just add to my knowledge that UndecidableInstances allows you to create non-terminating dictionaries in addition to the well-known risk of making the type checker loop. Thanks! / Emil Simon Peyton-Jones skrev:
It's a feature!
You have * B is a superclass of A * Eq is a superclass of B
So every A dictionary has a B dictionary inside it, and every B dictionary has an Eq dictionary inside it.
Now, your instance declaration instance (A a, Eq a) => B a says "if you give me an A dictionary and an Eq dictionary, I'll make you a B dictionary".
Now, 'test' needs a (B Int) dictionary. To get one, we need an (A Int) dictionary and an (Eq Int) dictionary. But
when solving these sub-problems, GHC assumes that you have in hand a solution to the original problem, this case (B Int)
Why? Read the SYB3 paper.
OK so now you see the problem: we can solve the (A Int) and (Eq Int) sub-problems by selection from the (B Int) dictionary.
Still, I confess that I have not fully grokked the relationship between the SYB3-style recursion stuff and the question of superclasses. So I will think about your example some more, thank you.
Meanwhile, it's clear that you are on thin ice.
Simon
| -----Original Message----- | From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe-bounces@haskell.org] On | Behalf Of Emil Axelsson | Sent: 22 January 2010 11:25 | To: Haskell Cafe | Subject: [Haskell-cafe] Non-termination due to context | | Hello all! | | Consider the following program: | | > {-# LANGUAGE FlexibleInstances, OverlappingInstances, UndecidableInstances #-} | > | > class B a => A a | > | > instance A Int | > | > class Eq a => B a | > | > instance (A a, Eq a) => B a | > | > eq :: B a => a -> a -> Bool | > eq = (==) | > | > test = 1 `eq` (2::Int) | | (This is a condensed version of a much larger program that I've been | debugging.) | | It compiles just fine, but `test` doesn't terminate (GHCi 6.10.4). If I | change the context `B a` to `Eq a` for the function `eq`, it terminates. | | Although I don't know all the details of the class system, it seems | unintuitive that I can make a program non-terminating just by changing | the context of a function (regardless of UndecidableInstances etc.). | | Is this a bug or a feature? | | / Emil | | _______________________________________________ | Haskell-Cafe mailing list | Haskell-Cafe@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe
Here's the relevant core for this file (GHC 6.10.4, so I'm a bit out of date):
Rec {
$dB_rh6 :: Undec.B GHC.Types.Int
[GlobalId]
[]
$dB_rh6 = $dB_rh6
end Rec }
Undec.test :: GHC.Bool.Bool
[GlobalId]
[]
Undec.test =
GHC.Classes.==
@ GHC.Types.Int
($dB_rh6
`cast` ((Undec.:Co:TB) GHC.Types.Int
:: (Undec.:TB) GHC.Types.Int ~ (GHC.Classes.:TEq) GHC.Types.Int))
(GHC.Types.I# 1)
(GHC.Types.I# 2)
The "cast" is saying that the dictionary for B is equivalent to the
dictionary for Eq (an optimization for empty classes with one
superclass, I guess).
"$dB_rh6" is the dictionary for B Int. GHC 'solves' this into a
classic looping program. I'm not sure how the derivation for this
dictionary goes.
-- ryan
so, given an A we can just pull the dictionary out of it
On Fri, Jan 22, 2010 at 3:24 AM, Emil Axelsson
Hello all!
Consider the following program:
{-# LANGUAGE FlexibleInstances, OverlappingInstances, UndecidableInstances #-}
class B a => A a
instance A Int
class Eq a => B a
instance (A a, Eq a) => B a
eq :: B a => a -> a -> Bool eq = (==)
test = 1 `eq` (2::Int)
(This is a condensed version of a much larger program that I've been debugging.)
It compiles just fine, but `test` doesn't terminate (GHCi 6.10.4). If I change the context `B a` to `Eq a` for the function `eq`, it terminates.
Although I don't know all the details of the class system, it seems unintuitive that I can make a program non-terminating just by changing the context of a function (regardless of UndecidableInstances etc.).
Is this a bug or a feature?
/ Emil
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (5)
-
Emil Axelsson -
Ivan Lazar Miljenovic -
Ross Paterson -
Ryan Ingram -
Simon Peyton-Jones