11.1.3 Examples of correct code using type quantifiers

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)