Тип возвращаемого значения метода не согласован

Question

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

type typExp =
  | TypInt
  | TypVar of char
  | Arrow of typExp * typExp
  | Lst of typExp;;

type substitution = (char * typExp) list;;

Я написал метод для выполнения замены переменной выражением типа с учетом правил подстановки замены типа.

let rec substitute (tau1 : typExp) (v : char) (tau2 : typExp) : typExp =
  match tau2 with
  |TypInt -> TypInt 
  |TypVar q -> (if(q=v) then tau1 else TypVar q)
  |Arrow (q,w) -> Arrow ((substitute tau1 v q), (substitute tau1 v w))
  |Lst q -> Lst (substitute tau1 v q)

;;

let rec applySubst (sigma: substitution) (tau: typExp) : typExp = 
  let reversedList = List.rev sigma in
  match reversedList with
  |(a,s)::w -> applySubst (List.rev w) (substitute s a tau)
  |[]->tau
;;

Я использовал эти методы для реализации функции проверки unifiable, однако, когда два типа не являются unifiable, он должен напечатать сообщение на экране, а метод print возвращает тип единицы, а не тип замены. Я не знаю, как с этим справиться.

let unify (tau1: typExp) (tau2:typExp) : substitution = 
  let rec helper acc t1 t2=
    match t1, t2 with
    | TypInt,TypInt -> acc(*not the problem*)
    | TypInt, TypVar q -> (q,TypInt)::acc
    | TypInt, Arrow (a,b) -> print_string "Not Unifyable" (* aproblem here*)
    | TypInt, Lst a -> print_string "Not Unifyable"
    | TypVar q, TypInt -> (q, TypInt)::acc
    | TypVar q, Arrow (a,s) -> (q,Arrow(a,s))::acc
    | TypVar q, Lst w -> (q, Lst w)::acc 
    | TypVar a, TypVar b ->( if(a=b) then acc else (a,TypVar b)::acc)
    | Arrow(q,w), Arrow(a,s) ->  if (helper [] w s)=[] then [] 
        else helper (helper [] w s) (applySubst (helper [] w s) q) (applySubst (helper [] w s) a)
    | Arrow (q,w), TypInt -> print_string "Not Unifyable"
    | Arrow (q,w), TypVar a -> (a, Arrow(q,w))::acc
    | Arrow (q,w), Lst a -> []
    | Lst q, TypInt -> []
    | Lst q, TypVar a -> (a,Lst q)::acc
    | Lst q, Arrow (s,t) -> []
    | Lst q, Lst w -> helper acc q w 
  in helper [] tau1 tau2

Мне интересно, не используя тип параметра, есть ли другой способ справиться с этим?

Answer 1

Если я понимаю ваш вопрос, вы пытаетесь решить, какое значение вернуть, если объединение невозможно. Это просто базовое проектное решение для вашей реализации, поэтому я не думаю, что есть один ответ, который кто-то может дать вам.

Вы можете определенно изменить тип функции на substitution option. Это хорошее чистое решение. Возвращаемое значение None будет означать, что объединение невозможно. Эти случаи будут выглядеть примерно так:

print_string "Not Unifyable"; None

Вы также можете поднять исключение для этого случая. В некоторых случаях это может быть очень эффективным решением, поскольку оно позволяет избежать выделения места для Some для всех успешных результатов (и работы по извлечению значения substitution). Однако разница во времени обычно не стоит дополнительной сложности обработки исключений (на мой взгляд).

Вы также можете просто вернуть пустой список. Это кажется менее чистым, поскольку это было бы законным результатом для нулевого объединения (я подозреваю).

Answer 2

Проблема связана с тем, что тип возвращаемого значения helper равен list of substitution, и некоторые из ваших совпадений возвращают не этот тип, а тип единицы измерения.Поэтому компилятор указывает на эту ошибку.

Теперь, один из способов исправить это вызвать исключение в этой точке.

 exception NotUnifiable;;

И заменить все строки, подобные:

    | TypInt, Arrow (a,b) -> print_string "Not Unifyable" 

Автор:

    | TypInt, Arrow (a,b) -> raise NotUnifiable

И использование унификации:

    try 
       unify ...the arguments...
    with NotUnifiable -> print "Not unifiable"

Но делать это может не то, что вы действительно хотите: как только возникает исключение,Вы останавливаете все.