11.3 Existentially typed data types

Type variables occurring in the body of a discriminated union type definition may be existentially quantified. Constructor definitions within discriminated union type definitions may be preceded by an existential type quantifier and followed by one or more existential type class constraints.

For example:

% A simple heterogeneous list type.
:- type list_of_any
    --->    nil_any
    ;       some [T] cons_any(T, list_of_any).

% A heterogeneous list type with a type class constraint.
:- typeclass showable(T) where [ func show(T) = string ].
:- type showable_list
    --->    nil
    ;       some [T] (cons(T, showable_list) => showable(T)).

% A different way of doing the same kind of thing, this
% time using the standard type list(T).
:- type showable
    --->    some [T] (s(T) => showable(T)).
:- type list_of_showable == list(showable).

% Here is an arbitrary example involving multiple type variables
% and multiple constraints.
:- typeclass foo(T1, T2) where [ /* … */ ].
:- type bar(T)
    --->    f1
    ;       f2(T)
    ;       some [T1] f3(T1)
    ;       some [T1, T2] f4(T1, T2, T) => (showable(T1), showable(T2))
    ;       some [T1, T2] f5(list(T1), T2) => fooable(T1, T2).

Construction and deconstruction of existentially quantified data types are inverses: when constructing a value of an existentially quantified data type, the “existentially quantified” functor acts for purposes of type checking like a universally quantified function: the caller will determine the values of the type variables. Conversely, for deconstruction the functor acts like an existentially quantified function: the caller must be defined so as to work for all possible values of the existentially quantified type variables which satisfy the declared type class constraints.

In order to make this distinction clear to the compiler, whenever you want to construct a value using an existentially quantified functor, you must prepend ‘new ’ onto the functor name. This tells the compiler to treat it as though it were universally quantified: the caller can bind that functor’s existentially quantified type variables to any type which satisfies the declared type class constraints. Conversely, any occurrence without the ‘new ’ prefix must be a deconstruction, and is therefore existentially quantified: the caller must not bind the existentially quantified type variables, but the caller is allowed to depend on those type variables satisfying the declared type class constraints, if any.

For example, the function ‘make_list’ constructs a value of type ‘showable_list’ containing a sequence of values of different types, all of which are instances of the ‘showable’ class

:- instance showable(int).
:- instance showable(float).
:- instance showable(string).

:- func make_list = showable_list.
make_list = List :-
	Int = 42,
	Float = 1.0,
	String = "blah",
	List =  'new cons'(Int,
		'new cons'(Float,
		'new cons'(String, nil))).

while the function ‘process_list’ below applies the ‘show’ method of the ‘showable’ class to the values in such a list.

:- func process_list(showable_list) = list(string).
process_list(nil) = "".
process_list(cons(Head, Tail)) = [show(Head) | process_list(Tail)].

There are some restrictions on the forms that existentially typed data constructors can take.

One restriction is that no type variable may be quantified both universally, by being listed as an argument of the type constructor, and existentially, by being listed in the existential type quantifier before the data constructor. The type ‘t12’ violates this restriction:

:- type t12(T)
    --->    f1(T)
    ;       some [T] f2(T).

The reason for the restriction is simple: without it, how can one decide whether the argument of ‘f2’ is universally or existentially quantified?

The other restriction is that every existentially quantified type variable must occur

• either in one of the argument types of the data constructor,
• or in one of the type class constraints on the data constructor, in the range of a functional dependency.

This means that the type ‘t3’ in

:- type t3
    --->    some [T1, T2] f5(T1) => xable(T1, T2).

violates this restriction unless the type class ‘xable’ has a functional dependency that determines the type bound to its second argument from the type bound to its first.

The reason for this restriction is that the identity of the type bound to the existential type variable must somehow be decided at runtime. It can either be given by the type of an argument, or determined through a functional dependency from the types bound to one or more other existential type variables.