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
Stefa
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
