-
Notifications
You must be signed in to change notification settings - Fork 54
Existential types
We know we can define a type for lists or other containers of a single type like this:
:- type list(T)
---> []
; [T | list(T)].As usual, type variables that occur in the body of the type definition must occur as arguments on the left side of the arrow. Such variables are universally quantified, meaning you can substitute any type for each of the variables to get a new type.
By design, all elements of a list(T) term must have the same type,
but what if you want a list in which the elements may have different types?
Rather than substituting for a single type variable, you would need
a distinct type variable for each element of the list. We can define a
suitable type using existentially quantified type variables
(or "existential types"):
:- type heterogeneous_list
---> nil
; some [T] cons(T, heterogeneous_list).The data constructors are named nil and cons just to distinguish them
from the usual lists.
The some VARS syntax before the data constructor introduces a
list of existentially quantified type variables. The definition of
heterogeneous_list says that each cons/2 constructor has a distinct
type variable T; the type variable is hidden within the data constructor.
Notice there is also no longer a universally quantified type variable on the
left side of the type definition.
For reasons we won't get into, to construct a term of an existentially quantified functor, you must prepend 'new ' to the functor name. For example:
List = 'new cons'(kitty, 'new cons'(doggy, nil))Deconstructing terms with existential types requires nothing special.
We could switch on the previously constructed List just as normal:
(
List = nil
;
List = cons(Head, _Tail),
...
)The thing that is a bit tricky is the type of Head. The actual type
of Head could be anything, depending on what List is bound to when
that code is executed. All we know is that Head has some type, which
is represented in Mercury as some [T] T.
Tip: sometimes you will get error messages from the compiler to the effect
of "expected some [T] T but got some [T] T". Don't be confused:
those are two distinct type variables, and the compiler is saying that they
might be bound to two different types.
The head/2 predicate for heterogeneous_list looks like this:
:- some [T] pred head(heterogeneous_list, T).
:- mode head(in, out) is semidet.
head(cons(Head, _Tail), Head).That's new. The type variable of the return argument had to be
existentially quantified. If the type variable were universally quantified
(the default behaviour), that means the caller should be able to call
head/2 with any type substituted for T. But we know that the type
of the return argument actually depends on what head/2 finds as the
first argument of the heterogeneous list.
What can you do with a term if you don't know its concrete type? For one, you
will have the type at run time so you can do things that only make use of the
run-time type information, such as print it out with io.write.
In most cases, you will probably want to perform a dynamic type check to see
if the term has a type that you were expecting. This can be done with the
builtin predicate dynamic_cast/2:
% dynamic_cast(X, Y) succeeds with Y = X iff X has the same ground type
% as Y (so this may succeed if Y is of type list(int), say, but not if
% Y is of type list(T)).
%
:- pred dynamic_cast(T1::in, T2::out) is semidet.Here is an example of its use:
( if
List = cons(Head, _Tail),
dynamic_cast(Head, Cat)
then
meow(Cat, !IO)
else
write_string("The first element is not a cat.\n", !IO)
)The standard library provides a "universal type" in the univ module that can
hold a term of any type:
% An object of type `univ' can hold the type and value of an object of any
% other type.
%
:- type univ.No surprises, internally it's a wrapper for an existential type.
:- type univ
---> some [T] univ_cons(T).The univ type is commonly used in the standard library when a universal type
is required. For example, any ground term can be thrown as an exception value
so when an exception is caught, the exception value is bound to a variable of
type univ.
You might wonder how data structures containing existential types are represented. A data constructor requires an extra memory word for each existentially quantified type variable that it contains. The extra word is used to store a pointer to a run-time representation of the type bound to that type variable, called a "type info".
So a univ term requires two words for the univ_cons/2 constructor.
The first word holds the type of the value inside the univ,
and the second word holds the value itself.
When you call dynamic_cast/2 it compares that the two type infos
of its input arguments represent the same type, otherwise it fails.
:- module exist_types.
:- interface.
:- import_module io.
:- pred main(io::di, io::uo) is det.
:- implementation.
:- type heterogeneous_list
---> nil
; some [T] cons(T, heterogeneous_list).
:- type dog
---> fido
; rex.
:- type cat
---> kitty
; tiger.
:- type rock
---> rocky.
main(!IO) :-
List = 'new cons'(tiger, 'new cons'(fido, 'new cons'(rocky, nil))),
print_list(List, !IO).
:- pred print_list(heterogeneous_list::in, io::di, io::uo) is det.
print_list(List, !IO) :-
( if head_tail(List, Head, Tail) then
( if dynamic_cast(Head, Dog) then
woof(Dog, !IO)
else if dynamic_cast(Head, Cat) then
meow(Cat, !IO)
else
write_string("Not a dog or cat!\n", !IO)
),
print_list(Tail, !IO)
else
write_string("The end.\n", !IO)
).
:- some [T] pred head_tail(heterogeneous_list, T, heterogeneous_list).
:- mode head_tail(in, out, out) is semidet.
head_tail(cons(Head, Tail), Head, Tail).
:- pred meow(cat::in, io::di, io::uo) is det.
meow(Cat, !IO) :-
(
Cat = kitty,
Name = "Kitty"
;
Cat = tiger,
Name = "Tiger"
),
write_string(Name, !IO),
write_string(" says meow!\n", !IO).
:- pred woof(dog::in, io::di, io::uo) is det.
woof(Dog, !IO) :-
(
Dog = fido,
Name = "Fido"
;
Dog = rex,
Name = "Rex"
),
write_string(Name, !IO),
write_string(" says woof!\n", !IO).