OCaml проверяет, существует ли элемент в правой части кортежа - PullRequest
Новая
       74

OCaml проверяет, существует ли элемент в правой части кортежа

0 голосов
/ 10 декабря 2018

В настоящее время я пытаюсь реализовать алгоритм вывода типов (алгоритм унификации) с использованием языка OCaml.Я столкнулся с некоторыми трудностями, связанными с реализацией, и надеялся, что кто-то будет достаточно любезен, чтобы оказать мне некоторую помощь.


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

[(TypeVar "t1", TypeFunc (TypeVar "t2", TypeVar "t3"))]

Этот тип (type * type) list является способом выражения равенства, так что тип t1 сопоставляется с функцией t2 -> t3.

Что я пытаюсьзахватить - это случай, когда переменная типа в левой части равенства также встречается в правой части, что приведет к сбою алгоритма.Для уточнения, если бы у нас было 

[(TypeVar "t1", TypeFunc (TypeVar "t1", TypeVar "t3"))]

, это дало бы нам ошибку, поскольку t1 = t1 -> t3 является противоречием.


Вот фактический OCamlФункция, которую я пытался реализовать, чтобы уловить это противоречие: 

let contradiction_check (a, t) =
  List.exists (fun (x, _) -> x = a) t;;

let t1 = TypeVar "t1";;
let t2 = TypeFunc (TypeVar "t2", TypeVar "t3");;

Проблема с этим кодом состоит в том, что прежде всего t2 не является списком, что может привести к ошибке.Однако это сделано намеренно, поскольку моя цель - взять список кортежей [(TypeVar "t1", TypeFunc (TypeVar "t2", TypeVar "t3"))] и проверить, находится ли левая сторона кортежа в правой части.

Я думаю, мой конкретный вопрос будет: Возможно ли реализовать функцию List.exists в качестве версии для кортежей?Я пробовал писать функции вручную, но это кажется более сложным, чем я думал.

Это особенно сложно для таких примеров, как: 

[(TypeVar "t1", TypeFunc (TypeFunc (TypeVar "t2", TypeVar "t3"),
  TypeFunc (TypeVar "t1", TypeVar "t4")))]

(** t1 = (t2 -> t3) -> (t1 -> t4) **)


Любые отзывы приветствуются.Спасибо.

1 Ответ

0 голосов
/ 10 декабря 2018

Вы должны просто написать рекурсивную функцию для поиска: 

(** [is_free ~varname t] is [true] iff [varname] appears as a free type variable in [t] *)
let is_free ~varname =
  let rec r = function
    | TypeVar n when String.( = ) n varname -> true
    | TypeVar _ -> false
    | TypeFunc s t -> r s || r t
    | TypaApp c t -> r c || r t (* if c is just a name not a type you don’t want [r c] here *)
    | TypeForall n t -> 
      if String.( = ) n varname
      then false
      else r t
  in
  r

Я не знаю, как выглядят все ваши случаи, но вы напишите функцию, похожую на приведенную выше.

Затем посмотрите, сможете ли вы объединить вещи: 

let can_unify = function
  | TypeVar t1, TypeVar t2 when String.( = ) t1 t2 -> (* decide what to do here *)
  | TypeVar varname, t -> not (is_free ~varname t)
  | _ -> (* throw an error or fix your types so this case can’t happen *)

Теперь вы можете достичь того, что хотите, с помощью знакомых функций списка.

...