anonymous variables in ocaml type inference

Question

I'm new to Ocaml and I've encountered a strange error when I was writing an interpreter for lambda calculus.

let rec valof : exp -> env -> value =
    fun exp env ->
    match exp with
      Var n -> exp2value (lookup env n)
    | Lambda (name , body) -> Clos (name , body , env) (*some thing wrong here*)
    |   _ -> Err
;;

exp, value and env are defined like:

type exp =
    Num of int
  | Str of string
  | Err
  | Var of string
  | Lambda of string * exp
  | App of exp * exp
;;

type value =
    Num of int
  | Str of string
  | Clos of string * exp * env
  | Err
;;

type env =
    Empty
  | Cons of string * exp * env
;;

When compiling, the compiler was complaining on the lambda line of the interpreter:

Error: This expression has type env/1490
       but an expression was expected of type env/1457

Any ideas where I screwed up? Thanks!

It means that env was declared twice, on different lines in different scopes. The two types have the same name, but are not equal. — Bergi
I'll find some proper references tomorrow and then write one. — Bergi

永劫回帰永劫回帰 · Accepted Answer · 2017-09-05T17:32:48

Error: This expression has type env/1490 
but an expression was expected of type env/1457

This kind of error is quite frequent when you debug your code in an interactive toplevel (REPL) and it means that you declared the type env twice. That can happen if you are copy-pasting your code in a REPL.

You don't need to append all those ;; after each statement. The OCaml compiler does not need them. Nevertheless, since ;; meaning it is useful in the toplevel and only there.

As you know, the first | can be omitted when you are doing a pattern matching or when you are defining a sum type. However, since you want to preserve the alignment in any case it is often considered as a good practice to include the | on each line even if it is not an obligation.

Here you're type are not mutually depend but value depends on exp and env, and depends on exp that means that you have to careful declare the types in the right order. But for clarity, you might want to present them in another order that can appear more logical. (I don't mean that this order is better than another I just want you to know that you can use the following syntax).

For example, if you want to present your type top-down (from the picture thing (ie. the environment) to the internal thing (ie. values)) you can use, the and syntax which tells the compiler that the types depend on each other.

type env =
  | Empty
  | Cons of string * exp * env

and exp =
  | Num of int
  | Str of string
  | Err
  | Var of string
  | Lambda of string * exp
  | App of exp * exp

and value =
  | Num of int
  | Str of string
  | Clos of string * exp * env
  | Err

Last thing, both value and exp contain the following constructors Num of int and Str of string, OCaml can't tell if Int 1 should be a value or an exp. More precisely, OCaml will choose that the constructor Int refers to env or exp (the one it will choose depends of the order in which you declared them). Thus it is advocated to choose different names for constructors.

anonymous variables in ocaml type inference

1 Answers