Next: , Previous: , Up: Existential types   [Contents]

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's an arbitrary example involving multiple
% type variables and multiple constraints.
:- typeclass foo(T1, T2) where [ /* … */ ].
:- type bar(T)
    --->    f1
    ;       f2(T)
    ;       some [T]
    ;       some [T1, T2]
            (f4(T1, T2, T) => showable(T1), showable(T2))
    ;       some [T1, T2]
            (f5(list(T1), T2) => fooable(T1, list(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 ‘list_of_showable’ 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(list_of_showable) = list(string).
process_list(nil) = "".
process_list(cons(Head, Tail)) = [show(Head) | process_list(Tail)].

Next: , Previous: , Up: Existential types   [Contents]