termination for FDs and ATs
Iavor Diatchki
iavor.diatchki at gmail.com
Wed May 3 17:03:48 EDT 2006
Hello,
On 5/3/06, Stefan Wehr <mail at stefanwehr.de> wrote:
> 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
I do not follow this example.
If we are trying to prove `D [Int]` we use the instance to reduce the
problem to `C Int`, and then we fail because we cannot solve this
goal.
If we are trying to validate the second instance, then we need to
prove that the context of the instance is sufficient to discharge the
super class requirements:
C a |- C (T [a]), F [a]
We can solve `F [a]` using the instance, and (by using the definition
of `T`) `C (T [a])` becomes `C a`, so we can solve it by assumption.
-iavor
More information about the Haskell-prime
mailing list