Interesting example. Yes, GHC builds recursive dictionaries these days. There's a bit of discussion in our SYB paper in ICFP'05. http://research.microsoft.com/%7Esimonpj/papers/hmap/ And Martin Sulzmann has a whole paper about this point. http://www.comp.nus.edu.sg/~sulzmann/ ("Co-induction...") Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Ross Paterson | Sent: 12 December 2005 10:46 | To: glasgow-haskell-users@haskell.org | Subject: instance inference | | I'm puzzled that the following is accepted. Is some sort of greatest | fixed point computation used for instances? | | {-# OPTIONS_GHC -fglasgow-exts #-} | module M where | | class C a b where c :: a -> b -> Bool | | instance C b b => C (Maybe a) b where c x y = c y y | | f :: Maybe a -> Bool | f x = c x x | | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
On Mon, Dec 12, 2005 at 03:38:18PM -0000, Simon Peyton-Jones wrote:
Interesting example. Yes, GHC builds recursive dictionaries these days. There's a bit of discussion in our SYB paper in ICFP'05. http://research.microsoft.com/%7Esimonpj/papers/hmap/ And Martin Sulzmann has a whole paper about this point. http://www.comp.nus.edu.sg/~sulzmann/ ("Co-induction...")
Should there be a -fallow-unsound-instances flag?
As a termination test, how about no restrictions on context and head except: Each assertion in the context must satisfy * the variables of the assertion are a sub-multiset of those of the head (though they may be the same), and * the assertion has fewer type constructors and variables (taken together and counting repetitions) than the head. This ensures that under any ground substitution the context assertion has fewer type constructors than the head. It would accept all instances accepted by the current test, plus instance C a instance C (s a) => C (Sized s a) instance (C1 a, C2 b) => C a b instance C1 Int a => C2 Bool [a] instance C1 Int a => C2 [a] b instance C a a => C [a] [a] But not things like instance (C1 a, C2 a, C3 a) => C a because that would need to check other instances as well.
A patch implementing a relaxed termination constraint is at http://www.soi.city.ac.uk/~ross/instance-termination.patch Here is the description: With -fglasgow-exts but not -fallow-undecidable-instances, GHC 6.4 requires that instances be of the following form: (1) each assertion in the context must constrain distinct variables mentioned in the head, and (2) at least one argument of the head must be a non-variable type. This patch replaces these rules with the requirement that each assertion in the context satisfy (1) no variable has more occurrences in the assertion than in the head, and (2) the assertion has fewer constructors and variables (taken together and counting repetitions) than the head. This allows all instances permitted by the old rule, plus such instances as instance C a instance Show (s a) => Show (Sized s a) instance (Eq a, Show b) => C2 a b instance C2 Int a => C3 Bool [a] instance C2 Int a => C3 [a] b instance C4 a a => C4 [a] [a] but still ensures that under any substitution assertions in the context will be smaller than the head, so context reduction must terminate. This is probably the best we can do if we consider each instance in isolation.
I have not followed this completely, but do these new rules now allow: class F a b c where f: a -> b -> c and then instance F a a a where ... which gives currenly gives (using -fglasgow-exts): Test.hs:6:0: Illegal instance declaration for `F a a a' (There must be at least one non-type-variable in the instance head Use -fallow-undecidable-instances to permit this) In the instance declaration for `F a a a' I recently ran into this, and I thought it to be perfectly reasonable, but GHC complained. On the other hand: instance F [a] [a] [a] where ... posed no problem, although I still see no non-type-variable in the head, or is [] a non-type-variable? I assumed the complaint was a left-over from the single parameter classes, where indeed having a single variable in an instance declaration does not make much sense. The second example does not follow the old rule (2) below! So rule (2) below is either not correctly implemented or not correctly stated or the error message is confusing, or I am missing something completely. Who can enlighten me? Doaitse because of the old rule (2) below. When I On 2006 feb 06, at 12:35, Ross Paterson wrote:
A patch implementing a relaxed termination constraint is at
http://www.soi.city.ac.uk/~ross/instance-termination.patch
Here is the description:
With -fglasgow-exts but not -fallow-undecidable-instances, GHC 6.4 requires that instances be of the following form:
(1) each assertion in the context must constrain distinct variables mentioned in the head, and
(2) at least one argument of the head must be a non-variable type.
On Mon, Feb 06, 2006 at 01:53:17PM +0100, Doaitse Swierstra wrote:
I have not followed this completely, but do these new rules now allow:
class F a b c where f: a -> b -> c
and then
instance F a a a where
Yes. Indeed they allow any unconstrained instance. They would also allow instance C a a => F a a a
On the other hand:
instance F [a] [a] [a] where ... posed no problem, although I still see no non-type-variable in the head, or is [] a non-type-variable? I assumed the complaint was a left-over from the single parameter classes, where indeed having a single variable in an instance declaration does not make much sense. The second example does not follow the old rule (2) below!
The argument [a] is not a type variable, so this is OK under the old rule (2).
Hello Ross, Monday, February 06, 2006, 2:35:40 PM, you wrote: RP> A patch implementing a relaxed termination constraint is at RP> http://www.soi.city.ac.uk/~ross/instance-termination.patch [this patch provides the following:] RP> With -fglasgow-exts but not -fallow-undecidable-instances RP> (1) no variable has more occurrences in the assertion than in the RP> head, and RP> (2) the assertion has fewer constructors and variables (taken together RP> and counting repetitions) than the head. i always thinks that existing rules too restrictive and something like just counting chars at the left and right should be used ;) one question - will be the same rules incorporated in Hugs? as you know, i'm trying to made Hugs+GHC compatible library, so this matters it will be even better if such improvement could be made to other Haskell compilers and included in Haskell-prime standard. class system of H98 and existing compilers is especially restricting flight of my imagination :) -- Best regards, Bulat mailto:bulatz@HotPOP.com
On Mon, Feb 06, 2006 at 05:49:42PM +0300, Bulat Ziganshin wrote:
one question - will be the same rules incorporated in Hugs? as you know, i'm trying to made Hugs+GHC compatible library, so this matters
Hugs does not attempt to restrict instances to enforce termination -- it just makes context reduction fail if it's taking too long (so any instance that's legal for GHC is also fine for Hugs). If some restriction is included in Haskell', then Hugs should implement it (but may continue to offer the other behaviour as an option).
participants (4)
-
Bulat Ziganshin -
Doaitse Swierstra -
Ross Paterson -
Simon Peyton-Jones