TypeFamilies vs. FunctionalDependencies & type-level recursion

[oleg at okmij.org]

I fully agree with Iavor. The correctness criterion is

the declaration 
	class C a b | a -> b

implies that the following implication must hold:
	C a1 b1, C a2 b2, a1 ~ a1 ===> b1 ~ b2

That implication lets us derive the proof of type equality, which we
can use for improving other types and resolving further constraints.

Here is a little Prolog program that helps us decide which instance
declarations should be accepted, and which are in error (regardless of
the Undecidable instances flag). The program currently works when
there is no overlapping. The program is a simple model checker for the
above implication.

Ex1: 

% class C a b | a -> b
% instance C Int Bool
% instance C a b

c(int,bool).
c(_A,_B).

?- c(X,Y), c(X,Y1), disunify(Y,Y1),
    print(['counterexample: ', c(X,Y), c(X,Y1)]).
%% [counterexample: , c(int, bool), c(int, e7)]

A counter-example was found. The instances must be rejected.


Ex2:
> Wait.  What about
> 	instance C [a] [b]

% class C a b | a -> b
% instance C Int Bool
% instance C [a] [b]

c(int,bool).
c([_A],[_B]).

?- c(X,Y), c(X,Y1), disunify(Y,Y1),
    print(['counterexample: ', c(X,Y), c(X,Y1)]).
%% [counterexample: , c([_G2442], [e8]), c([_G2442], [e9])]

Reject.


Ex3:
% class C a b | a -> b
% instance C Int Bool
% instance C [a] a

c(int,bool).
c([_A],_A).

?- c(X,Y), c(X,Y1), disunify(Y,Y1),
   print(['counterexample: ', c(X,Y), c(X,Y1)]).
%% No counter-examples.

Accept.


Ex4:
> What about the following code--do you think this should be illegal,
> too?
> 	class C a b c | a -> b where
> 	instance C (Maybe a) (Maybe b) (Maybe b) where

c(maybe(_A),maybe(_B),maybe(_B)).

?- c(X,Y,Z), c(X,Y1,Z1), disunify(Y,Y1),
   print(['counterexample: ', c(X,Y,Z), c(X,Y1,Z1)]).

%% [counterexample: , c(maybe(_G2446), maybe(e11), maybe(e11)), 
%%	              c(maybe(_G2446), maybe(e12), maybe(e12))]

Illegal.


Ex5:
> But now you are going to end up rejecting programs like this:
> 	class C a b | a -> b
> 	class D a b | a -> b
> 	instance (D a b) => C [a] [b]


d(int,bool). % Need an instance for D; otherwise, we won't type check.
c([A],[B]) :- d(A,B).

?- c(X,Y), c(X,Y1), disunify(Y,Y1),
   print(['counterexample: ', c(X,Y), c(X,Y1)]).
%% Failed, no counter-examples.

Accepted.


Ex6:
%% class C a a' b | a a' -> b 
%% class D a b | a -> b
%% instance (D a b) => C [a] [a'] [b]

d(int,bool). % Need an instance for D; otherwise, we won't type check.
c([A],[A1],[B]) :- d(A,B).


?- c(X,Y,Z), c(X1,Y1,Z1), [X,Y] = [X1,Y1], disunify(Z,Z1),
    print(['counterexample: ', c(X,Y,Z), c(X1,Y1,Z1)]).
%% Failed to find a counter-example.

Accept.



Here is the definition of disunify.

eigen(X) :- gensym(e,X).

% Ground a term, instantiating all of its variables to fresh constants
instantiate(T) :- term_variables(T,Vars), maplist(eigen,Vars).

% disunify(T1,T2)
% Holds if T1 and T2 are not unifiable, or can be made non-unifiable. 
% If succeeds, T1 and T2 are ground and T1 \= T2.

disunify(T1,T2) :-
  instantiate(T1),
  copy_term(T2,T21),
  (T1 = T21 -> instantiate(T2), \+ (T1=T2); true).