[mercury-users] Mode problem

[Ralph Becket]

Lauri Alanko, Thursday, 28 November 2002:
> Hello.
> 
> I just started learning Mercury. For starters, I tried to implement
> simple type inference for simply-typed lambda calculus with ints and
> bools.
[...]
> 
> Here's a shot at doing it in Mercury:
> 
[...]
> 
> The problem is that --infer-modes cannot figure out a sensible mode for
> tc, and neither can I. The first argument to tc is clearly "in" (I don't
> want a theorem prover), but the environment and type are both likely to
> get "partially bound" during the course of the inference, and I cannot
> figure out the correct mode to express this.
> 
> So is there a sensible mode for tc, or is there another way how these
> things should be done in Mercury?

For efficiency reasons, Mercury does not support Herbrand constraints
(i.e. Prolog style logic variables).

If you look at the term library module, you'll find that it implements
everything you need, including unification.  However, you'll need to
explicitly pass the substitution around.  Look at samples/interpreter.m
for an example of how to do it.

- Ralph
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------