[Haskell-cafe] Re: Resolving overloading loops for circular constraint graph

[Martin Sulzmann]

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