Manuel M T Chakravarty <[EMAIL PROTECTED]> wrote:: > 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?
Indeed, the equality is used backwards, so you aren't missing something. I tried to find an example for which both directions of the equality are relevant but failed. Of course, this is not a proof. Stefan _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org//mailman/listinfo/haskell-prime
