Stefan Wehr: > Manuel M T Chakravarty <[EMAIL PROTECTED]> wrote:: > > > Martin Sulzmann: > >> Manuel M T Chakravarty writes: > >> > Martin Sulzmann: > >> > > A problem with ATs at the moment is that some terminating FD programs > >> > > result into non-terminating AT programs. > >> > > > >> > > Somebody asked how to write the MonadReader class with ATs: > >> > > > >> http://www.haskell.org//pipermail/haskell-cafe/2006-February/014489.html > >> > > > >> > > This requires an AT extension which may lead to undecidable type > >> > > inference: > >> > > > >> http://www.haskell.org//pipermail/haskell-cafe/2006-February/014609.html > >> > > >> > The message that you are citing here has two problems: > >> > > >> > 1. You are using non-standard instances with contexts containing > >> > non-variable predicates. (I am not disputing the potential > >> > merit of these, but we don't know whether they apply to Haskell' > >> > at this point.) > >> > 2. You seem to use the super class implication the wrong way around > >> > (ie, as if it were an instance implication). See Rule (cls) of > >> > Fig 3 of the "Associated Type Synonyms" paper. > >> > > >> > >> I'm not arguing that the conditions in the published AT papers result > >> in programs for which inference is non-terminating. > >> > >> We're discussing here a possible AT extension for which inference > >> is clearly non-terminating (unless we cut off type inference after n > >> number of steps). Without these extensions you can't adequately > >> encode the MonadReader class with ATs. > > > > This addresses the first point. You didn't address the second. let me > > re-formuate: I think, you got the derivation wrong. You use the > > superclass implication the wrong way around. (Or do I misunderstand?) > > I think the direction of the superclass rule is indeed wrong. But what about > the following example: > > class C a > class F a where type T a > instance F [a] where type T [a] = a > class (C (T a), F a) => D a where m :: a -> Int > instance C a => D [a] where m _ = 42 > > If you now try to derive "D [Int]", you get > > ||- D [Int] > subgoal: ||- C Int -- via Instance > subgoal: ||- C (T [Int]) -- via Def. of T in F > subgoal: ||- D [Int] -- Superclass
You are using `T [a] = a' *backwards*, but the algorithm doesn't do that. Or am I missing something? Manuel _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org//mailman/listinfo/haskell-prime