termination for FDs and ATs
Iavor Diatchki
iavor.diatchki at gmail.com
Tue May 9 13:31:15 EDT 2006
Hello,
On 5/9/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
> But there is also the equality `T [Int] = Int` which we could apply.
I think I see what you mean. Here is what I worked out in case anyone
else didn't follow.
The axioms from the above declarations are:
1. forall a. F [a]
2. forall a. F [a] => T [a] = a
3. forall a. D a => C (T a) /\ F a
4. forall a. C a => D [a]
"proof"
goal: D [Int]
Using 4 with a = Int:
goal: C Int
Use (3 with a = [Int]) and (2 with a = Int) to get a new rule:
5. D [Int] /\ F [Int] => C Int /\ F [Int]
Using 5 and projection:
goal: F [Int], D [Int]
Using 1 with a = Int:
goal: D [Int]
Now we are back to where we started. In this case we can notice this
and give up, but in general this might be tricky.
-Iavor
More information about the Haskell-prime
mailing list