The Mercury Language Reference Manual: Some idioms using existentially quantified types

The standard library module ‘univ’ provides an abstract type named ‘univ’ which can hold values of any type. You can form heterogeneous containers (containers that can hold values of different types at the same time) by using data structures that contain univs, e.g. ‘list(univ)’.

% `univ' is a type which can hold any value.
:- type univ.

% The function univ/1 takes a value of any type and constructs
% a `univ' containing that value (the type will be stored along
% with the value)
:- func univ(T) = univ.

% The function univ_value/1 takes a `univ' argument and extracts
% the value contained in the `univ' (together with its type).
% This is the inverse of the function univ/1.
:- some [T] func univ_value(univ) = T.

The ‘univ’ type in the standard library is in fact a simple example of an existentially typed data type. It could be implemented as follows:

:- implementation.
:- type univ
    --->    some [T] mkuniv(T).
univ(X) = 'new mkuniv'(X).
univ_value(mkuniv(X)) = X.

An existentially typed procedure is not allowed to have different types for its existentially typed arguments in different clauses or in different subgoals of a single clause. For instance, both of the following examples are illegal:

:- some [T] pred bad_example(string, T).

bad_example("foo", 42).
bad_example("bar", "blah").
    % type error (cannot unify `int' and `string')

:- some [T] pred bad_example2(string, T).

bad_example2(Name, Value) :-
    ( Name = "foo", Value = 42
    ; Name = "bar", Value = "blah"
    ).
    % type error (cannot unify `int' and `string')

However, using ‘univ’, it is possible for an existentially typed function to return values of different types at each invocation.

:- some [T] pred good_example(string, T).

good_example(Name, univ_value(Univ)) :-
    ( Name = "foo", Univ = univ(42)
    ; Name = "bar", Univ = univ("blah")
    ).

Using ‘univ’ doesn’t work if you also want to use type class constraints. If you want to use type class constraints, then you must define your own existentially typed data type, analogous to ‘univ’, and use that:

:- type univ_showable
    --->    some [T] (mkshowable(T) => showable(T)).

:- some [T] pred harder_example(string, T) => showable(T).

harder_example(Name, Showable) :-
    ( Name = "bar", Univ = 'new mkshowable'(42)
    ; Name = "bar", Univ = 'new mkshowable'("blah")
    ),
    Univ = mkshowable(Showable).

:- some [T] pred bad_example3(string, T).
:-         mode bad_example3(in(bound("foo")), out) is det.
:-          mode bad_example3(in(bound("bar")), out) is det.
:- pragma promise_pure(bad_example3/2).
bad_example3("foo"::in(bound("foo")), 42::out).
bad_example3("bar"::in(bound("bar")), "blah"::out).
    % type error (cannot unify `int' and `string')

The solution is similar, although in this case an intermediate predicate is required:

:- some [T] pred good_example3(string, T).
:-          mode good_example3(in(bound("foo")), out) is det.
:-          mode good_example3(in(bound("bar")), out) is det.
good_example3(Name, univ_value(Univ)) :-
	good_example3_univ(Name, Univ).

:- pred good_example3_univ(string, univ).
:- mode good_example3_univ(in(bound("foo")), out) is det.
:- mode good_example3_univ(in(bound("bar")), out) is det.
:- pragma promise_pure(good_example3_univ/2).
good_example3_univ("foo"::in(bound("foo")), univ(42)::out).
good_example3_univ("bar"::in(bound("bar")), univ("blah")::out).

11.4 Some idioms using existentially quantified types