Next: Examples of incorrect code using type quantifiers, Previous: Semantics of type quantifiers, Up: Existentially typed predicates and functions [Contents]
Here are some examples of type-correct code using universal and existential types.
/* simple examples */ :- pred foo(T). foo(_). % ok :- pred call_foo. call_foo :- foo(42). % ok (T = int) :- some [T] pred e_foo(T). e_foo(X) :- X = 42. % ok (T = int) :- pred call_e_foo. call_e_foo :- e_foo(_). % ok /* examples using higher-order functions */ :- func bar(T, T, func(T) = int) = int. bar(X, Y, F) = F(X) + F(Y). % ok :- func call_bar = int. call_bar = bar(2, 3, (func(X) = X*X)). % ok (T = int) % returns 13 (= 2*2 + 3*3) :- some [T] pred e_bar(T, T, func(T) = int). :- mode e_bar(out, out, out(func(in) = out is det)). e_bar(2, 3, (func(X) = X * X)). % ok (T = int) :- func call_e_bar = int. call_e_bar = F(X) + F(Y) :- e_bar(X, Y, F). % ok % returns 13 (= 2*2 + 3*3)