miniTypeChecker.ml

open Core.Std

module MiniTypeChecker = struct
  type t = U | Int | Bool | A of t * t
  type e = Var of string | Abs of string * t * e | App of e * e
  let compose_types x y = match (x,y) with (_,U) -> U | (U,_) -> U | _ -> A (x,y)
  let apply_types x y = match x with A (a,b) -> if a = y then b else U | _ -> U
  let get_type ctx = function
    | "T" -> Bool | "F" -> Bool
    | x -> try int_of_string x |> ignore ; Int
           with _ -> (match List.Assoc.find ctx x with Some t -> t | None -> U)
  let rec infer ctx = function
    | Var x       -> get_type ctx x
    | Abs (x,t,e) -> compose_types t @@ infer (List.Assoc.add ctx x t) e
    | App (e,e')  -> apply_types (infer ctx e) (infer ctx e')
  let rec to_str = function
    | U -> "" | Int -> "int" | Bool -> "bool"
    | A (t,u) -> "("^(to_str t)^" -> "^(to_str u)^")"
  let type_check x = match to_str @@ infer [] x with "" -> None | s -> Some s
end