CODEWITHSUNDEEP
typesocamltype-inference
Wayne Hong
Wayne Hong

Reputation: 119

I don't agree with this type inference

I'm trying to write an OCaml evaluator in OCaml. Basically I need to imitate OCaml's typechecker. I have the following code, which should return a type but the compiler complains of type mismatch. 

let rec typecheck (expr:moexpr) (tenv:type environment) =
  match expr with
  | ...
  | Match(e, (pat, exp)::l) -> let etype=(typecheck e tenv) in
  (List.fold_left (fun (cp, ce) fp -> (typecheck ce (matchtype tenv cp etype))) 
    (typecheck exp tenv) (pat, exp)::l)

In my fold left I give the base as (typecheck exp tenv) which should be a motype (my type type). The error is that the fold left function (typecheck ce (matchtype tenv cp etype)) evaluates to a motype, not surprising, but that the expected type is mopat * moexpr - mopat is my pattern type. Shouldn't the value of a fold left operation be the base type and the function return type?

Upvotes: 0

Views: 119

Answers (1)

camlspotter
camlspotter

Reputation: 9030

Since you are writing a type checker, I think I do not need to explain how the type inference works here.

Check the type of fold_left. It takes a function whose first element is the accumulator, and your "base" is the initial accumulator. Your accumulator has the form (cp, ce) so its type is mopat * moexpr, but your base acc has motype. I guess the arguments are missordered. Flip (cp,ce) and fp then it looks better. You still have a problem of fp, the real accumulator, which is never used.

Upvotes: 3

Related Questions