I am using SML to design a compiler for another functional language (you can see its definition here http://corelab.postech.ac.kr/~hanjun/2016S_compiler/hw/fun_language_definition.php). My task is to design a typechecking.
What is return type?
if a>0 then <<3, 4>, 5> else <<6>, 7, 8>
For answering this question, I need to find "join" of the 2 type above. "Join": is the least common supertype. For example, t1 <: t3 and t2 <: t3 => t3 is a join(t1,t2).
"Meet" is most common subtype. t3 <: t1 and t3 <: t2 => t3 is a meet(t1, t2).
My task to design meet and join mutually recursive. Could you please give me a hint how to implement them?
You'll need to study the sub-typing rules to deduce the recursive definition. For an example, use tuple types. Since longer tuples are subtypes of shorter ones, given that the common prefix types match, and one tuple type is a subtype of anther if the element types are pairwise sub-types, you'll have:
join(<t1, ... tm>, <u1, ... un>) = <join(t1,u1), ... join(tp,up)>
where p = min(m,n)
and
meet(<t1, ... tm>, <u1, ... un>) = <meet(t1,u1), ... meet(tm,um), u_m+1, ... un>
when (wlog) m <= n
Most of the rules will be self-recursive like this. The exception will be function types due to parameter inversion. Here you'll need meet to define join and vice-versa. I won't spoil your fun by giving the answer.
The base cases are of course just
meet(int, int) = join(int, int) = int