[Haskell-cafe] Re: Resolving overloading loops for circular
constraint graph
Martin Sulzmann
martin.sulzmann.haskell at googlemail.com
Thu Sep 10 14:54:50 EDT 2009
2009/9/9 Stefan Holdermans <stefan at cs.uu.nl>
> Dear Martin,
>
> By "black-holing" you probably mean co-induction. That is,
>> if the statement to proven appears again, we assume it must hold.
>> However, type classes are by default inductive, so there's no
>> easy fix to offer to your problem.
>>
>
> A propos: are there fundamental objections to coinductive resolving, i.e.,
> constructing recursive dictionaries. I suppose termination is hard to
> guarantee then: is it enough to require constraints to be productive w.r.t.
> instance heads?
>
>
Yes, you need instances to be productive, otherwise, you get
bogus cyclic proofs like
instance Foo a => Foo a
dictFooa = dictFooa
You could call this a bug, or simply blame the programmer
for writing down a 'bogus' instance.
Under co-inductive type class solving more (type class) programs will
terminate (my guess). Here are some references:
Satish R. Thatte: Semantics of Type Classes Revisited. LISP and Functional
Programming 1994<http://www.informatik.uni-trier.de/%7Eley/db/conf/lfp/lfp1994.html#Thatte94>:
208-219
As far as I know, the first paper which talks about co-induction and type
classes.
I myself and some co-workers explored this idea further in some
unpublished draft:
AUTHOR = {M. Sulzmann and J. Wazny and P. J. Stuckey},
TITLE = {Co-induction and Type Improvement in Type Class Proofs},
NOTE = {Manuscript},
YEAR = {2005},
MONTH = {July},
PS = {http://www.cs.mu.oz.au/~sulzmann/manuscript/coind-type-class-proofs.ps
<http://www.cs.mu.oz.au/%7Esulzmann/manuscript/coind-type-class-proofs.ps>}
I'm quite fond of co-induction because it's such an elegant and powerful
proof technique. However, GHC's co-induction mechanism is fairly limited,
see Simon's reply, so I'm also curious to see what's happening in the
future.
-Martin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090910/c259bd76/attachment-0001.html
More information about the Haskell-Cafe
mailing list