2009/9/9 Stefan Holdermans <ste...@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
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users