[mercury-users] Mode problem

[Lauri Alanko]

Hello.

I just started learning Mercury. For starters, I tried to implement
simple type inference for simply-typed lambda calculus with ints and
bools. In Prolog it would go like this:


lookup([(K,V)|_],K,V) :- !.
lookup([_|Rest],K,V) :- lookup(Rest,K,V).

tc(t,bool,_).
tc(f,bool,_).
tc(C,int,_) :- integer(C).
tc(V,T,Env) :- atom(V), lookup(Env,V,T).
tc(if(Test,Then,Else),T,Env) :-
	tc(Test,bool,Env),
	tc(Then,T,Env),
	tc(Else,T,Env).
tc(app(F,X),T,Env) :-
	tc(F,fun(S,T),Env),
	tc(X,S,Env).
tc(lambda(V,X),fun(S,T),Env) :-
	atom(V),
	tc(X,T,[(V,S)|Env]).


Here's a shot at doing it in Mercury:


:- type ident == string.

:- type typ ---> 
	int;
	bool;
	fun(typ,typ).

:- type value --->
	int(int);
	bool(bool).

:- type expr --->
	variable(ident);
	lambda(ident,expr);
	app(expr,expr);
	const(value);
	if(expr,expr,expr).

:- type env == list({ident,typ}).

:- pred lookup(list({K,V}),K,V).
lookup([{K,V}|_],K,V) :- !.
lookup([_|Rest],K,V) :- lookup(Rest,K,V).

:- pred tc(expr,typ,env).
tc(const(int(_)),int,_).
tc(const(bool(_)),bool,_).
tc(variable(X),T,Env) :- lookup(Env,X,T).
tc(app(F,E),T,Env) :- 
	tc(E,S,Env),
	tc(F,fun(S,T),Env).
tc(lambda(X,E),fun(S,T),Env) :- 
	tc(E,T,[{X,S}|Env]).
tc(if(C,X,Y),T,Env) :- 
	tc(C,bool,Env),
	tc(X,T,Env),
	tc(Y,T,Env).


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?


Lauri Alanko
la at iki.fi
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------