%% -*- prolog -*-

mem(X,[X|_]).
mem(X,[_,L]) :- mem(X,L).

% match:
%  mem(a,L)
%  mem(X,[X|L])
% must distinguish logically distinct variables of same name
%  mem(a,L_1)
%  mem(X,[X|L_2])
% these are identical if:
%  X=a
%  L_1=[a|L_2]
% Figuring out what values must be assigned to which variables
% in order to get two expressions containing "named holes", ie,
% logic variables, is called "unification".

%%% type inference in programming language: ML, Haskell,
%%%  C++ templates, C# (upcoming release)

%%% idea:
%%%  - define baby strongly typed programming langauge
%%%  - write prolog relation typed(P) which says that P
%%%    is valid program, w/ correct types.
%%%  - put logical variables where types belong: type inference!

%%% baby language:
%%%  - expressions
%%%      <expr> ::= <num> | <func_call>
%%%      <num>  ::= 0 | 1 | 2
%%%      <func_call> ::= [<expr>, <expr>]
%%%  - all functions are curried.
%%%  - type annotations all over!
%%%     sin(a)
%%%    annotate with types all over!
%%%     ((sin:T1)(  (a:T2) )):T3
%%%  - modify syntax of language for type annotations
%%%      
%%%      <program> ::= <aexpr>
%%%      <aexpr> ::= t(<vexpr>,<type>)
%%%      <vexpr> ::= <num> | <func_call>
%%%      <num>   ::= 0 | 1 | 2
%%%      <func_call> ::= [<aexpr>, <aexpr>]
%%%      <type> ::= int | f(<type>,<type>)

typed(t(N,int)) :- member(N,[0,1,2]).
typed(t([t(Ef,f(Ta,Tres)), t(Ea,Ta)], Tres)) :- typed(t(Ef,f(Ta,Tres))), typed(t(Ea,Ta)).
typed(t(negate,f(int,int))).
typed(t(plus,f(int,f(int,int)))).

% | ?- typed(t([t(negate,_), t(2,_)],T)).    

% T = int ? ;

% | ?- typed(t([t(plus,_), t(2,_)],T)).  

% T = f(int,int) ? ;

% | ?- typed(t([t([t(plus,_), t(2,_)],_), t(1,_)],T)). 

% T = int ? ;
