Circular Instance Declarations
When -fallow-undecidable-instances is switched on, is there any reason why circular instances are forbidden? For instance: module CircularInsts where { data D r = ZeroD | SuccD (r (D r)); instance (Eq (r (D r))) => Eq (D r) where { ZeroD == ZeroD = True; (SuccD a) == (SuccD b) = a == b; _ == _ = False; }; newtype C a = MkC a deriving Eq; equalDC :: D C -> D C -> Bool; equalDC = (==); } When I compile this, I get this: $ ghc -fglasgow-exts -fallow-undecidable-instances -c CircularInsts.hs CircularInsts.hs:2: Context reduction stack overflow; size = 21 Use -fcontext-stack20 to increase stack size to (e.g.) 20 `Eq (C (D C))' arising from use of `==' at CircularInsts.hs:16 `Eq (D C)' arising from use of `==' at CircularInsts.hs:16 `Eq (C (D C))' arising from use of `==' at CircularInsts.hs:16 `Eq (D C)' arising from use of `==' at CircularInsts.hs:16 Would it be reasonable for the compiler to check back through the stack and allow the circularity? It will just create an ordinary recursive function. -- Ashley Yakeley, Seattle WA
Hi Ashley See the thread "Type Class Problem". In his post on Aug 22 Simon Peyton-Jones said that it shouldn't be hard to implement, and mentioned that it would ruin the property that dictionaries can be evaluated by call-by-value. I couldn't puzzle out enough of the type class system to make the change on my first try, and since then I've been looking for a more general solution Actually, I'm surprised someone else has a use for this. I wanted circular instances for playing with the paper "Recursion Schemes from Comonads". What are you trying to do? Detecting circularity in a derivation is equivalent to accepting a regular infinite derivation for instances. Would you have a use for irregular derivations? Brandon On Sat, 6 Sep 2003, Ashley Yakeley wrote:
When -fallow-undecidable-instances is switched on, is there any reason why circular instances are forbidden? For instance:
module CircularInsts where { data D r = ZeroD | SuccD (r (D r));
instance (Eq (r (D r))) => Eq (D r) where { ZeroD == ZeroD = True; (SuccD a) == (SuccD b) = a == b; _ == _ = False; };
newtype C a = MkC a deriving Eq;
equalDC :: D C -> D C -> Bool; equalDC = (==); }
When I compile this, I get this:
$ ghc -fglasgow-exts -fallow-undecidable-instances -c CircularInsts.hs CircularInsts.hs:2: Context reduction stack overflow; size = 21 Use -fcontext-stack20 to increase stack size to (e.g.) 20 `Eq (C (D C))' arising from use of `==' at CircularInsts.hs:16 `Eq (D C)' arising from use of `==' at CircularInsts.hs:16 `Eq (C (D C))' arising from use of `==' at CircularInsts.hs:16 `Eq (D C)' arising from use of `==' at CircularInsts.hs:16
Would it be reasonable for the compiler to check back through the stack and allow the circularity? It will just create an ordinary recursive function.
-- Ashley Yakeley, Seattle WA
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
In article <Pine.GSO.4.44.0309072012230.3951-100000@blinky>, Brandon Michael Moore <brandon@its.caltech.edu> wrote:
Actually, I'm surprised someone else has a use for this. I wanted circular instances for playing with the paper "Recursion Schemes from Comonads". What are you trying to do?
It's for HScheme. The Object type has a pluggable reference type, so that both IO-based and pure functional Scheme variants are possible. The general idea is something like this: data Object ref = NilObject | PairObject (ref (Object ref)) (ref Object ref)); instance (Eq (ref (Object ref))) => Eq (Object ref) where etc. newtype Constant a = MkConstant a deriving Eq; equalConstant :: Object Constant; equalConstant = (==); equalIORef :: Object IORef; equalIORef = (==); -- Ashley Yakeley, Seattle WA
In article <Pine.GSO.4.44.0309072012230.3951-100000@blinky>, Brandon Michael Moore <brandon@its.caltech.edu> wrote:
Detecting circularity in a derivation is equivalent to accepting a regular infinite derivation for instances. Would you have a use for irregular derivations?
Could you give me an example? -- Ashley Yakeley, Seattle WA
On Sun, 7 Sep 2003, Ashley Yakeley wrote:
In article <Pine.GSO.4.44.0309072012230.3951-100000@blinky>, Brandon Michael Moore <brandon@its.caltech.edu> wrote:
Detecting circularity in a derivation is equivalent to accepting a regular infinite derivation for instances. Would you have a use for irregular derivations?
Could you give me an example?
I should have asked whether you needed irregular types, and "undecidable" instances for irregular types. I'm close to a proof that will justify more permissive instances for regular types (plus a bit), but I haven't made much progress on irregular types. I'm wondering if anyone actually uses them, let alone fancy instances for them. Also, if I tried to expand my approach to irregular types it would require generating dictionaries a runtime, rather than just defining dictionaries recursively. In case the word irregular is the problem I'll give my definition, and how I'm applying it to types. The definition is from Pierce, in "Types and Programming Languages". An irregular tree is a tree with an infinite number of distinct subtrees. When I say a type is irregular I mean the infinite trees you get when you (recursively) expand all the applications of type constructors is irregular. A simple irregular type is Irr a = Con a (Irr (F a)) (as long as F uses a) This expands to something like <a|<F a|F (F a)| ...>>, where <t|t..t> denotes a sum type. Each right child is like the parent with an extra F everywhere, so the tree is irregular. The sort of instance I'm interested in is something like instance (Eq a,Eq (Irr (F a)) => Eq (Irr a) where the context only mentions (subexpressions of) type expressions encoutered while expanding the type. Are you using anything like this? Brandon
In article <Pine.GSO.4.44.0309091136120.26237-100000@clyde>, Brandon Michael Moore <brandon@its.caltech.edu> wrote:
A simple irregular type is Irr a = Con a (Irr (F a)) (as long as F uses a)
Would this be an irregular type, with F as ((->) val)? data SymbolExpression sym val a = ClosedSymbolExpression a | OpenSymbolExpression sym (SymbolExpression sym val (val -> a)); I used to use this in HScheme for expressions with free variables, as in the lambda calculus. For instance, "\x.xy" has "y" as a free variable, and might be represented as something like this: OpenSymbolExpression "y" (ClosedSymbolExpression (\y -> (\x -> x y))) It's very clean and safe, and can be made an instance of FunctorApplyReturn, but it turned out to be a bit slow. I also tried this: data ListSymbolExpression sym val a = MkListSymbolExpression [sym] ([val] -> a); MkListSymbolExpression ["y"] (\[y] -> (\x -> x y)) This is much simpler, but now one has to make sure that the lists are the same size, so to speak. But this one turned out to be the fastest: newtype FuncSymbolExpression sym val a = MkFuncSymbolExpression ((sym -> val) -> a); MkFuncSymbolExpression (\f -> (\x -> x (f "y"))) The downside is that there's no way to find out what the free variables are. That's OK for Scheme, however, since Scheme doesn't complain about unbound variables until run-time. So, um, any excuse to talk about HScheme anyway. -- Ashley Yakeley, Seattle WA
On Wed, 10 Sep 2003, Ashley Yakeley wrote:
Brandon Michael Moore <brandon@its.caltech.edu> wrote:
A simple irregular type is Irr a = Con a (Irr (F a)) (as long as F uses a)
Would this be an irregular type, with F as ((->) val)?
data SymbolExpression sym val a = ClosedSymbolExpression a | OpenSymbolExpression sym (SymbolExpression sym val (val -> a));
This would be an irregular type. In my proposal an instance declaration deriving some instance of SymbolExpression sym val a could use the types sym val and a in the context, but not (val -> a) which would only arise from unfolding the type constructor. Of course when I say "proposal" I mean "Would be a proposal if only I could prove that last lemma".
I used to use this in HScheme for expressions with free variables, as in the lambda calculus. For instance, "\x.xy" has "y" as a free variable, and might be represented as something like this:
OpenSymbolExpression "y" (ClosedSymbolExpression (\y -> (\x -> x y)))
It's very clean and safe, and can be made an instance of FunctorApplyReturn, but it turned out to be a bit slow. I also tried this:
data ListSymbolExpression sym val a = MkListSymbolExpression [sym] ([val] -> a);
MkListSymbolExpression ["y"] (\[y] -> (\x -> x y))
This is much simpler, but now one has to make sure that the lists are the same size, so to speak. But this one turned out to be the fastest:
newtype FuncSymbolExpression sym val a = MkFuncSymbolExpression ((sym -> val) -> a);
MkFuncSymbolExpression (\f -> (\x -> x (f "y")))
The downside is that there's no way to find out what the free variables are. That's OK for Scheme, however, since Scheme doesn't complain about unbound variables until run-time.
So, um, any excuse to talk about HScheme anyway.
It looks like your scheme puts the type system to good use. I used a value type with numbers, Val->Val functions, and some other stuff. I gave up when I realized I needed to thread references through everything to implement R5RS. I suppose everyone has started a Scheme in Haskell sometime. Brandon
A simple irregular type is Irr a = Con a (Irr (F a)) (as long as F uses a)
The sort of instance I'm interested in is something like instance (Eq a,Eq (Irr (F a)) => Eq (Irr a) where the context only mentions (subexpressions of) type expressions encoutered while expanding the type.
Are you using anything like this?
In Haskell terms (making things slightly more general): data Irr a f = Con a (Irr (f a)) instance (Eq a,Eq (Irr (f a)) => Eq (Irr a f) The above instance is inherently dangerous (cause context reduction becomes non-terminating). I haven't seen the code attached to the instance. My guess is that if you could state something like the following instance (Eq a, (forall b. Eq b => Eq (f b))) => Eq (Irr a f) then your code type checks. Note that the above instance declaration is terminating. Unfortunately, such an extension does not exist at the moment. However, you can encode the above in ordinary Haskell. Check out Valery Trifonov's Haskell'03 paper "Simulating Quantified Class Constraints". Martin
I have also wanted this, in the context of John Hughes' restricted data types. In order to simulate these properly, you need circular instances of this form. - Hal On Sun, 2003-09-07 at 21:07, Brandon Michael Moore wrote:
Hi Ashley
See the thread "Type Class Problem". In his post on Aug 22 Simon Peyton-Jones said that it shouldn't be hard to implement, and mentioned that it would ruin the property that dictionaries can be evaluated by call-by-value. I couldn't puzzle out enough of the type class system to make the change on my first try, and since then I've been looking for a more general solution
Actually, I'm surprised someone else has a use for this. I wanted circular instances for playing with the paper "Recursion Schemes from Comonads". What are you trying to do?
Detecting circularity in a derivation is equivalent to accepting a regular infinite derivation for instances. Would you have a use for irregular derivations?
Brandon
On Sat, 6 Sep 2003, Ashley Yakeley wrote:
When -fallow-undecidable-instances is switched on, is there any reason why circular instances are forbidden? For instance:
module CircularInsts where { data D r = ZeroD | SuccD (r (D r));
instance (Eq (r (D r))) => Eq (D r) where { ZeroD == ZeroD = True; (SuccD a) == (SuccD b) = a == b; _ == _ = False; };
newtype C a = MkC a deriving Eq;
equalDC :: D C -> D C -> Bool; equalDC = (==); }
When I compile this, I get this:
$ ghc -fglasgow-exts -fallow-undecidable-instances -c CircularInsts.hs CircularInsts.hs:2: Context reduction stack overflow; size = 21 Use -fcontext-stack20 to increase stack size to (e.g.) 20 `Eq (C (D C))' arising from use of `==' at CircularInsts.hs:16 `Eq (D C)' arising from use of `==' at CircularInsts.hs:16 `Eq (C (D C))' arising from use of `==' at CircularInsts.hs:16 `Eq (D C)' arising from use of `==' at CircularInsts.hs:16
Would it be reasonable for the compiler to check back through the stack and allow the circularity? It will just create an ordinary recursive function.
-- Ashley Yakeley, Seattle WA
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell -- -- Hal Daume III | hdaume@isi.edu "Arrest this man, he talks in maths." | www.isi.edu/~hdaume
participants (4)
-
Ashley Yakeley -
Brandon Michael Moore -
Hal Daume III -
Martin Sulzmann