[mercury-users] type error with existentially typed data structure

[Simon Taylor]

On 07-Sep-2001, Peter Ross <peter.ross at miscrit.be> wrote:
> On Thu, Sep 06, 2001 at 05:06:39PM +0200, Peter Ross wrote:
> > With the attached file I get the following type error, and I am a bit
> > lost as to why it occurs.
> > 
> > petri.m:125: In clause for predicate `petri:bind_env/4':
> > petri.m:125:   in unification of variable `Env'
> > petri.m:125:   and term `BindEnv(Token)':
> > petri.m:125:   type error in argument(s) of higher-order term (with arity 1).
> > petri.m:125:   Functor (BindEnv) has type `((func T) = int)',
> > petri.m:125:   expected type was `((func V_9) = int)';
> > petri.m:125:   argument 1 (Token) has type `T',
> > petri.m:125:   expected type was `V_9'.
> > For more information, try recompiling with `-E'.
> 
> Problem found.  Don't use the automatically generated accessor functions
> with existentially quantified data structures.

Just to clarify this, the automatically generated accessor functions do
work with existentially typed data structures.

The problem in Peter's case was that if a constructor has two existentially
typed fields, if you extract them in separate unifications or field
accessor calls, the type-checker isn't smart enough to work out that
the existentially quantified type variables from the two unifications
or field accessor calls are the same. In cases like this you may
need to write out the unifications by hand, instead of using field
accessors.

For example:

:- type existential_pair
        ---> some [T] existential_pair(
                        first :: T,
                        second :: T
             ).

:- import_module std_util.

	% Extracting a single field is OK.
:- some [T] func get_first(existential_pair) = T.
get_first(ExistPair) = ExistPair ^ first.

        % The compiler can't work out that the two `T's are the same:
	%
	% test.m:024: In clause for function `existential_pair_to_pair_1/1':
	% test.m:024:   in unification of variable `Pair'
	% test.m:024:   and term `(First - Second)':
	% test.m:024:   type error in argument(s) of functor `-/2'.
	% test.m:024:   Argument 1 (First) has type `T',
	% test.m:024:   expected type was `T';
	% test.m:024:   argument 2 (Second) has type `T',
	% test.m:024:   expected type was `T'.
:- some [U] func existential_pair_to_pair_1(existential_pair) = pair(T).
existential_pair_to_pair_1(ExistPair) = Pair :-
	First = ExistPair ^ first,
	Second = ExistPair ^ second,
	Pair = First - Second.

        % This is equivalent to existential_pair_to_pair_1 after expansion
        % of the automatically generated accessor functions.
	%
	% test.m:033: In clause for function `existential_pair_to_pair_2/1':
	% test.m:033:   in unification of variable `Pair'
	% test.m:033:   and term `(First - Second)':
	% test.m:033:   type error in argument(s) of functor `-/2'.
	% test.m:033:   Argument 1 (First) has type `T',
	% test.m:033:   expected type was `T';
	% test.m:033:   argument 2 (Second) has type `T',
	% test.m:033:   expected type was `T'.
:- some [U] func existential_pair_to_pair_2(existential_pair) = pair(T).
existential_pair_to_pair_2(ExistPair) = Pair :-
        ExistPair = existential_pair(First, _),
        ExistPair = existential_pair(_, Second),
	Pair = First - Second.

        % OK.
:- some [U] func existential_pair_to_pair_3(existential_pair) = pair(U).
existential_pair_to_pair_3(ExistPair) = Fst - Snd :-
        ExistPair = existential_pair(Fst, Snd).


Simon.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------