termination for FDs and ATs
Stefan Wehr
mail at stefanwehr.de
Tue May 9 04:40:42 EDT 2006
Manuel M T Chakravarty <chak at cse.unsw.edu.au> wrote::
> Stefan Wehr:
>> Manuel M T Chakravarty <chak at cse.unsw.edu.au> 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
More information about the Haskell-prime
mailing list