% Model checking of Functional Dependencies % % Given a Haskell multi-parameter type-class declaration and a set % of its instances, we check if the instances conform to the functional % dependency defined for the type class arguments. % The type class declaration % class C a b | a -> b % implies that the following implication must hold: % C a1 b1, C a2 b2, a1 == a1 ===> b1 == b2 % % We search for the violation of the above implication; if found, % we report the counter-example. % Ground a term, instantiating all of its variables to fresh constants % (so to make the printout nicer) eigen(X) :- gensym(t,X). instantiate(T) :- term_variables(T,Vars), maplist(eigen,Vars). % Mark some predicates as dynamic so we can write several examples in % the same file, deleting the previous definitions. ?- dynamic c/3, c/4, d/3, d/4. cleanup :- % Start with the clean slate retractall(c(_,_,_)), retractall(c(_,_,_,_)), retractall(d(_,_,_,_)), retractall(d(_,_,_)). ?- print('\nExample 1\n'). % (Most of the examples are due to David Mazi`eres, posted on the % Haskell-Prime mailing list in June 2011) % This example involves overlapping instances % class C a b | a -> b % instance C Bool Int % instance C a b % The encoding of the instances % The first argument is the identifier of the instance. % Underscored variables are singleton variables % (if we omit the underscores, we get an warning from the interpreter). c(i1,bool,int). c(i2,_A,_B). % searching for the counter-example ?- G = (c(_,X,Y), c(_,X,Y1)), G, Y \== Y1, % evaluate the goal, check the negation of the constr print('counterexample: '), instantiate(G), print(G), nl. %% counterexample: c(i1, bool, int), c(i2, bool, t1) %% A counter-example was found: the type class constraint C Bool a %% can be resolved either by choosing the first instance (C Bool Int) %% or the second instance (C a b) where a is Bool and b is some type t1, %% which is not Int. %% Since the counter-example was found, the program must be rejected. ?- print('\nExample 2\n'). ?- cleanup. % This example has no overlapping between instances % class C a b | a -> b % instance C Bool Int % instance C [a] [b] c(i1,bool,int). c(i2,[_A],[_B]). ?- G = (c(_,X,Y), c(_,X,Y1)), G, Y \== Y1, print('counterexample: '), instantiate(G), print(G), nl. %% counterexample: c(i2, [t2], [t3]), c(i2, [t2], [t4]) %% Reject. ?- print('\nExample 3\n'). ?- cleanup. % class C a b | a -> b % instance C Bool Int % instance C [a] a c(i1,bool,int). c(i2,[A],A). ?- G = (c(_,X,Y), c(_,X,Y1)), G, Y \== Y1, print('counterexample: '), instantiate(G), print(G), nl. %% No counter-examples were found: Accept the program. ?- print('\nExample 4\n'). ?- cleanup. % class C a b c | a -> b where % instance C (Maybe a) (Maybe b) (Maybe b) where c(i,maybe(_A),maybe(B),maybe(B)). ?- G = (c(_,X,Y,_Z), c(_,X,Y1,_Z1)), G, Y \== Y1, print('counterexample: '), instantiate(G), print(G), nl. %% counterexample: c(i, maybe(t5), maybe(t6), maybe(t6)), %% c(i, maybe(t5), maybe(t7), maybe(t7)) ?- print('\nExample 5\n'). ?- cleanup. % Several type classes % class C a b | a -> b % class D a b | a -> b % instance (D a b) => C [a] [b] d(d,bool,int). % Need an instance for D; otherwise, nothing to select c(c(Id),[A],[B]) :- d(Id,A,B). ?- G = (c(_,X,Y), c(_,X,Y1)), G, Y \== Y1, print('counterexample: '), instantiate(G), print(G), nl. %% Failed, no counter-examples. ?- print('\nExample 6\n'). ?- cleanup. % A functional dependency among several variables % class C a a' b | a a' -> b % class D a b | a -> b % instance (D a b) => C [a] [a'] [b] d(d,bool,int). % Need an instance for D; otherwise, nothing to select c(c(Id),[A],[_A1],[B]) :- d(Id,A,B). ?- G = (c(_,X,Y,Z), c(_,X1,Y1,Z1)), G, [X,Y] = [X1,Y1], Z \== Z1, print('counterexample: '), instantiate(G), print(G), nl. %% Failed to find a counter-example. ?- print('\nExample 7\n'). ?- cleanup. % class C a b | a -> b % instance C [a] [b] % instance C [m a] [Either b c] % instance C [[a]] [Either a c] c(c1,[_A],[_B]). c(c2,[A],[either(_B,_C)]) :- composite(A). c(c3,[[A]],[either(A,_C)]). composite([_X]). composite(either(_X,_Y)). ?- G = (c(_,X,Y), c(_,X,Y1)), G, Y \== Y1, print('counterexample: '), instantiate(G), print(G), nl. %% counterexample: c(c1, [t8], [t9]), c(c1, [t8], [t10]) ?- print('\nExample 8\n'). ?- cleanup. % Example by Wolfgang Jeltsch, Haskell list, 2003 % class C a b c | a b -> c where % f :: a -> b -> c % instance C a b c => C a (x,y,b) c where % f a (_,_,b) = f a b % instance C a (a,c,b) c where % f _ (_,c,_) = c c(c2, A,tup(A,C,_B), C). c(c1(I),A,tup(_X,_Y,B),C) :- c(I,A,B,C). ?- G = (c(_,X,Y,Z), c(_,X,Y,Z1)), G, Z \== Z1, print('counterexample: '), instantiate(G), print(G), nl. %% counterexample: c(c2, t11, tup(t11, t12, tup(t11, t13, t14)), t12), %% c(c1(c2), t11, tup(t11, t12, tup(t11, t13, t14)), t13)