Определение типа для лямбда-выражений в Ocaml - PullRequest
Новая
       2

Определение типа для лямбда-выражений в Ocaml

3 голосов
/ 10 сентября 2011

На практике я пытаюсь определить тип, соответствующий выражениям лямбда-исчисления, состоящим из переменных, абстракций и приложений. Моя текущая лучшая попытка: 

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

Однако я хотел бы ограничить первую часть Abs значением Var. Например, я хотел бы, чтобы это было плохо сформированное выражение: 

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

но в настоящее время оно считается действительным. Я также хотел бы потребовать, чтобы первая часть App была Abs. Есть ли способ заставить систему типов применять эти ограничения, или это толкает ее за пределы того, для чего она была предназначена?

Редактировать: Если неясно, Abs(Var "x", Var "x") следует считать действительным.

Ответы [ 4 ]

4 голосов
/ 10 сентября 2011

Вы не можете заставить систему типов напрямую применять что-то подобное.Вместо этого я хотел бы рассмотреть определение двух типов: 

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

Это похоже на ответ Джеффа, но дает вам свободу изменять тип, используемый для определяющих переменных, не беспокоясь о его изменении в двух местах.Оба являются правильными способами решения проблемы.

2 голосов
/ 10 сентября 2011

Полиморфные варианты позволяют вам определять подтипы типов данных.Подтипы применяют простые структурные ограничения.

Например, вот определение лямбда-терминов с полиморфными вариантами с определением подтипа для нормальных форм головы. 

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))
2 голосов
/ 10 сентября 2011

AFAIU, вам нужны GADT для достижения того, что недавно было объединено в ствол SVN.

Вот пример любителя (возможно, не совсем правильный, но он удовлетворяет вашим требованиям): 

        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")
1 голос
/ 10 сентября 2011

Проблема в том, что вы определили Abs, чтобы принять два expr с, и каждый из них может быть Var, Abs или App.

Тяга Abs должнасостоят из переменной и выражения, а не двух выражений.В этом случае переменная - это просто строка, поэтому ваш Abs должен состоять из строки и выражения.

Измените его на: 

Abs of string * expr
...