Next: Type conversions, Previous: Type classes, Up: Top [Contents]
Existentially quantified type variables (or simply “existential types” for short) are useful tools for data abstraction. In combination with type classes, they allow you to write code in an “object oriented” style that is similar to the use of interfaces in Java or abstract base classes in C++.
Mercury supports existential type quantifiers on predicate and function declarations, and in data type definitions. You can put type class constraints on existentially quantified type variables.
Type variables in type declarations for polymorphic predicates or functions are normally universally quantified. However, it is also possible to existentially quantify such type variables, by using an explicit existential quantifier of the form ‘some Vars’ before the ‘pred’ or ‘func’ declaration, where Vars is a list of variables.
For example:
% Here the type variables `T' is existentially quantified :- some [T] pred foo(T). % Here the type variables `T1' and `T2' are existentially quantified. :- some [T1, T2] func bar(int, list(T1), set(T2)) = pair(T1, T2). % Here the type variable `T2' is existentially quantified, % but the type variables `T1' and `T3' are universally quantified. :- some [T2] pred foo(T1, T2, T3).
Explicit universal quantifiers, of the form ‘all Vars’, are also permitted on ‘pred’ and ‘func’ declarations, although they are not necessary, since universal quantification is the default. (If both universal and existential quantifiers are present, the universal quantifiers must precede the existential quantifiers.) For example:
% Here the type variable `T2' is existentially quantified, % but the type variables `T1' and `T3' are universally quantified. :- all [T3] some [T2] pred foo(T1, T2, T3).
If a type variable in the type declaration for a polymorphic predicate or function is universally quantified, this means the caller will determine the value of the type variable, and the callee must be defined so that it will work for all types which are an instance of its declared type.
For an existentially quantified type variable, the situation is the converse: the callee must determine the value of the type variable, and all callers must be defined so as to work for all types which are an instance of the called procedure’s declared type.
When type checking a predicate or function, if a variable has a type that occurs as a universally quantified type variable in the predicate or function declaration, or a type that occurs as an existentially quantified type variable in the declaration of one of the predicates or functions that it calls, then its type is treated as an opaque type. This means that there are very few things which it is legal to do with such a variable — basically you can only pass it to another procedure expecting the same type, unify it with another value of the same type, put it in a polymorphic data structure, or pass it to a polymorphic procedure whose argument type is universally quantified. (Note, however, that the standard library includes some quite powerful procedures such as ‘io.write’ which can be useful in this context.)
A non-variable type (i.e. a type that is not a type variable) is considered more general than an existentially quantified type variable. Type inference will therefore never infer an existentially quantified type for a predicate or function unless that predicate or function calls (directly or indirectly) a predicate or function which was explicitly declared to have an existentially quantified type.
Note that an existentially typed procedure is not allowed to have different types for its existentially typed arguments in different clauses (even mode-specific clauses) or in different subgoals of a single clause; however, the same effect can be achieved in other ways (see Some idioms using existentially quantified types).
For procedures involving calls to existentially-typed predicates or functions,
the compiler’s mode analysis must take account
of the modes for type variables in all polymorphic calls.
Universally quantified type variables have mode in,
whereas existentially quantified type variables have mode out.
As usual, the compiler’s mode analysis
will attempt to reorder the elements of conjunctions
in order to satisfy the modes.
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)
Here are some examples of code using universal and existential types that contains type errors.
/* simple examples */
:- pred bad_foo(T).
bad_foo(42).
% type error
:- some [T] pred e_foo(T).
e_foo(42).
% ok
:- pred bad_call_e_foo.
bad_call_e_foo :- e_foo(42).
% type error
:- some [T] pred e_bar1(T).
e_bar1(42).
e_bar1(42).
e_bar1(43).
% ok (T = int)
:- some [T] pred bad_e_bar2(T).
bad_e_bar2(42).
bad_e_bar2("blah").
% type error (cannot unify types `int' and `string')
:- some [T] pred bad_e_bar3(T).
bad_e_bar3(X) :- e_foo(X).
bad_e_bar3(X) :- e_foo(X).
% type error (attempt to bind type variable `T' twice)
Existentially quantified type variables are especially useful in combination with type class constraints.
Type class constraints can be either universal or existential. Universal type class constraints are written using ‘<=’, as described in Type class constraints on predicates and functions; they signify a constraint that the caller must satisfy. Existential type class constraints are written in the same syntax as universal constraints, but using ‘=>’ instead of ‘<=’; they signify a constraint that the callee must satisfy. If a declaration has both universal and existential constraints, then the existential constraints must precede the universal constraints.
For example:
% Here `c1(T2)' and `c2(T2)' are existential constraints, % and `c3(T1)' is a universal constraint, :- all [T1] some [T2] ((pred p(T1, T2) => (c1(T2), c2(T2))) <= c3(T1)).
Existential constraints must only constrain type variables that are explicitly existentially quantified. Likewise, universal constraints must only constrain type variables that are universally quantified, although in this case the quantification does not have to be explicit because universal quantification is the default (see Syntax for explicit type quantifiers).
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.
The first 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: the reference of ‘T’ in the ‘f2’ data constructor being simultaneously inside the scope of more than quantification can mislead readers who see one of the quantifications, and stop looking for the other. The simplest way to avoid such confusion is to require the programmer to avoid having one quantification shadow another.
The second restriction is that type variables listed in the existential type quantifier before the data constructor cannot be repeated. Type variables in the argument list of the type constructor also cannot be repeated, whether or not the data constructors of that type have existential types. The type ‘t34’ violates both these restrictions:
:- type t34(A, B, A)
---> f3(A, B)
; some [C, D, D] f4(C, D).
The third and final restriction is that every existentially quantified type variable must occur
This means that the type ‘t5’ in
:- type t5
---> 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.
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)’.
The interface to ‘univ’ includes the following:
% `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’ does not 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).
The issue can also arise for mode-specific clauses (see Different clauses for different modes). For instance, the following example is illegal:
:- 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).
Previous: Existentially typed data types, Up: Existential types [Contents]