Ggtcf

I'm writing a function in OCaml to check whether two types are unifiable and will produce a unifier if there is one or print the appropriate message.
Here is the type system :

type typExp =
 | TypInt
 | TypVar of char
 | Arrow of typExp * typExp
 | Lst of typExp;;

type substitution = (char * typExp) list;;

I wrote a method to perform substitution of a variable by a type expression given substitution rules of type substitution.

let rec substitute (tau1 : typExp) (v : char) (tau2 : typExp) : typExp =
 match tau2 with
 |TypInt -> TypInt 
 |TypVar q -> (if(q=v) then tau1 else TypVar q)
 |Arrow (q,w) -> Arrow ((substitute tau1 v q), (substitute tau1 v w))
 |Lst q -> Lst (substitute tau1 v q)

;;

let rec applySubst (sigma: substitution) (tau: typExp) : typExp = 
 let reversedList = List.rev sigma in
 match reversedList with
 |(a,s)::w -> applySubst (List.rev w) (substitute s a tau)
 |[]->tau
;;

I used those methods to implement the unifiable check function, however, when two types are not unifiable, it should print a message on the screen and the print method return a unit type not of that of substitution. I don't know how to deal with that.

let unify (tau1: typExp) (tau2:typExp) : substitution = 
 let rec helper acc t1 t2=
 match t1, t2 with
 | TypInt,TypInt -> acc(*not the problem*)
 | TypInt, TypVar q -> (q,TypInt)::acc
 | TypInt, Arrow (a,b) -> print_string "Not Unifyable" (* aproblem here*)
 | TypInt, Lst a -> print_string "Not Unifyable"
 | TypVar q, TypInt -> (q, TypInt)::acc
 | TypVar q, Arrow (a,s) -> (q,Arrow(a,s))::acc
 | TypVar q, Lst w -> (q, Lst w)::acc 
 | TypVar a, TypVar b ->( if(a=b) then acc else (a,TypVar b)::acc)
 | Arrow(q,w), Arrow(a,s) -> if (helper [] w s)=[] then [] 
 else helper (helper [] w s) (applySubst (helper [] w s) q) (applySubst (helper [] w s) a)
 | Arrow (q,w), TypInt -> print_string "Not Unifyable"
 | Arrow (q,w), TypVar a -> (a, Arrow(q,w))::acc
 | Arrow (q,w), Lst a -> []
 | Lst q, TypInt -> []
 | Lst q, TypVar a -> (a,Lst q)::acc
 | Lst q, Arrow (s,t) -> []
 | Lst q, Lst w -> helper acc q w 
 in helper [] tau1 tau2

I'm wondering without using option type, is there another way to deal with this?

The issue is due to the fact that the return type of helper is a list of substitution and some of your match do not return this type but the unit type instead. Therefore, the compiler points this error.

Now, one way to fix that is to raise an exception at those point.

 exception NotUnifiable;;

And replace all lines similar to :

 | TypInt, Arrow (a,b) -> print_string "Not Unifyable" 

By :

 | TypInt, Arrow (a,b) -> raise NotUnifiable

And the usage of unify:

 try 
 unify ...the arguments...
 with NotUnifiable -> print "Not unifiable"

But doing this may not be what you really want : as soon as there is an exception, you stop everything.

If I understand your question, you're trying to decide what value to return when unification isn't possible. This is just a basic design decision for your implementation, so I don't think there's one answer that anyone can give you.

You can definitely change the function's type to substitution option. That is a nice clean solution. The return value of None would indicate that unification isn't possible. These cases would look something like this:

print_string "Not Unifyable"; None

You could also raise an exception for this case. That can be a very effective solution in some cases, as it avoids allocating space for Some for all the successful results (and the work to extract the substitution value). However, the difference in time is usually not worth the extra complexity of dealing with exceptions (in my opinion).

You could also just return an empty list. This feels less clean, as it would be a legitimate result for a null unification (I suspect).