Defining a type for lambda expressions in Ocaml

For practice, I'm trying to define a type corresponding to lambda-calculus expressions composed of variables, abstractions, and applications. My current best attempt is:

开发者_StackOverflow社区

type expr = Var of string | Abs of expr * expr | App of expr * expr

However, I would like to restrict the first part of an Abs to be a Var. For instance, I would like this to be an ill-formed expr:

Abs(Abs(Var "foo", Var "bar"), Var "bar")

but it is currently accepted as valid. I would also like to require that the first part of an App be an Abs. Is there any way to have the type system enforce these restrictions, or is this pushing it beyond what it was designed to do?

Edit: In case it wasn't clear, Abs(Var "x", Var "x") should be considered valid.

---

You can't get the type system to directly enforce something like that. Instead, I would consider defining two types:

type variable = Name of string
type expr = Var of variable | Abs of variable * expr | App of expr * expr

This is similar to Jeff's answer, but gives you the freedom to change the type used for the defining variables without having to worry about changing it in two places. Both are valid ways to go about dealing with the problem.

---

AFAIU, you need GADTs to achieve that, which were recently merged into svn trunk.

Here is amateur's example (maybe not fully correct, but it satisfies your requirements) :

        OCaml version 3.13.0+dev6 (2011-07-29)

# type _ t =
  | Var : string -> string t
  | Abs : (string t * 'a t) -> (string * 'a) t
  | App : ((string * 'a) t * 'b t) -> ('a -> 'b) t;;
type 'a t =
    Var : string -> string t
  | Abs : (string t * 'b t) -> (string * 'b) t
  | App : ((string * 'c) t * 'd t) -> ('c -> 'd) t
# Abs(Abs(Var "foo", Var "bar"), Var("bar"));;
Error: This expression has type (string * 'a) t
       but an expression was expected of type string t
# App(Var "bar", Abs(Var "foo", Var "bar"));;
Error: This expression has type string t
       but an expression was expected of type (string * 'a) t
# App(Abs(Var "foo", Var "bar"), Var("bar"));;
- : (string -> string) t = App (Abs (Var "foo", Var "bar"), Var "bar")

---

Polymorphic variants let you define subtypes of datatypes. The subtypes enforce simple structural constraints.

For example, here's a definition of lambda-terms with polymorphic variants, with a definition of a subtype for head normal forms.

type var = [ `Var of string ]

type expr = [
  | var
  | `Abs of var * expr
  | `App of expr * expr
  ]

type irr (*non-head-reducible applications*) = [
  | var
  | `App of irr * expr
  ]
type hnf (*head normal forms*) = [
  | irr
  | `Abs of var * hnf
  ]

let substitution (x : var) (u : expr) : expr -> expr =
  failwith "left as an exercise"

(*Iterated head reductions produce a head normal form*)
let rec head_reductions : expr -> hnf = function
  | #var as x -> x
  | `Abs (x, u) -> `Abs (x, head_reductions u)
  | `App (u, v) ->
      match head_reduction u with
      | #irr as u -> u
      | `Abs (x, w) -> head_reductions (substitution x u (w :> expr))

---

The problem is you've defined Abs to accept two exprs and each of those may be Var, Abs or App.

An Abstraction should consist of a variable and expression, not two expressions. A variable is just a string in this case so your Abs should consist of a string and expression.

Change it to:

Abs of string * expr