OCaml GADTs - сопоставление с образцом соответствует неверному типу аргумента - PullRequest
Новая
       42

OCaml GADTs - сопоставление с образцом соответствует неверному типу аргумента

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

Мне нужно реализовать идеально сбалансированное двоичное дерево (или PBT для краткости), используя обобщенные алгебраические типы данных .Я понял, как работают GADT в целом, и (несколько некрасиво) синтаксис, который я должен использовать, чтобы он работал в OCaml.Затем я должен реализовать некоторые функции, которые работают с ним.Прямо сейчас у меня проблема с функцией, которая принимает два PBT, у которых целые числа хранятся в их узлах, и возвращает PBT, который хранит в своих узлах сумму каждого из соответствующих узлов.Хорошо.Звучит достаточно просто.Это код, который я написал для типа данных PBT: 

(*Important in order to define the index of the level of our perfectly 
balanced tree*)
(*Natural numbers, Peano style (now with GADTs)*)
type zero = Zero
type _ succ = Succ : 'natural -> 'natural succ

(*Implementing the perfectly balanced binary tree - or PBTree - with GADTs*)
(*'a -> type of tree | _ -> index of level*)

type ('a, _) pbtree =
(*Base case: empty tree - level 0, rock-bottom*)
EmptyTree : ('a, zero) pbtree
(*Inductive case: regular PBTree - tree on the left, value, tree on the 
right*)          
| PBTree : ('a, 'natural) pbtree * 'a * ('a, 'natural) pbtree -> ('a, 
'natural succ) pbtree

Это сработало до сих пор.Тип компилируется, и мне даже удалось выполнить функцию переворота (вернуть зеркальное отображение PBT).Теперь настоящая проблема исходит от этого маленького парня: 

let rec add : type int natural. 
(int, natural) pbtree -> (int, natural) pbtree -> (int, natural) pbtree =
function
| EmptyTree, EmptyTree -> EmptyTree
| PBTree(left1, value1, right1), PBTree(left2, value2, right2) -> 
PBTree((add left1 left2), value1 + value2, (add right1, right2))

Прямо там, где я делаю сопоставление с образцом для пустого дерева, это дает мне следующую ошибку: 

| EmptyTree, EmptyTree -> EmptyTree

Error: This pattern matches values of type 'a*'b
       but a pattern was expected which matches values of type
         (int, natural) pbtree

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

let rec add : type int natural. (int, natural) pbtree * (int, natural)         
pbtree -> (int, natural) pbtree =
function
| EmptyTree, EmptyTree -> EmptyTree
| PBTree(left1, value1, right1), PBTree(left2, value2, right2) -> 
PBTree((add (left1, left2)), value1 + value2, (add (right1, right2)))

Однако это не то, что я должен делать.Моя функция должна принимать два аргумента.Даже с этой модификацией, которая решает головоломку парного типа, она выдаст следующую ошибку: 

Error: This pattern matches values of type int/1805
        but an expression was expected of type int/1

Итак, первый подход, который я выбрал, - это лучшее, что я могу сделать.Мой вопрос: почему сопоставление с образцом обнаруживает пару, когда ее явно нет?Почему он не может обнаружить два аргумента, как это обычно должно быть?Это способ, которым я написал функцию для обнаружения этого паттерна?

Если я, гипотетически, использовал второй подход при создании функции (тот, в котором она использовала пару PBT в качестве аргумента вместо двух аргументов -два PBT), то почему он не распознает целочисленное значение, которое я пытаюсь дать ему для вычисления?Может быть, это из-за того, что он слишком инструментирован для работы?

Я не могу понять, что здесь пошло не так, и если я попытаюсь изменить тип, чтобы ослабить это синтаксическое ограничение, то я рискну создать PBT, который нарушает егособственное определение просто из-за типа, допускающего ветви, которые имеют неравный размер.

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

1 Ответ

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

Последняя ошибка, которую вы получаете: 

Error: This pattern matches values of type int/1805
       but an expression was expected of type int/1

говорит о том, что есть два разных типа int, которые не совместимы, и дает вам их внутренние идентификаторы, чтобы вы могли различать их.Эта ошибка возникает из-за того, что type int natural. создает два новых локально абстрактных типа в области действия функции, которая будет скрывать любые другие типы с этими именами в этой области.Чтобы устранить эту ошибку, просто не создавайте локально абстрактный тип с именем int.Затем он будет ограничивать переменную типа фактическим типом int, как и предполагалось.

Другая ошибка: 

Error: This pattern matches values of type 'a*'b
       but a pattern was expected which matches values of type
         (int, natural) pbtree

происходит потому, что EmptyTree, EmptyTree на самом деле равно шаблон, который соответствует паре.В OCaml кортежи не требуют скобок, если они разделены другими способами.Так что это, например, допустимый (и чрезвычайно запутанный) литерал типа (int * int) list: [1, 2; 3, 4; 5, 6].

function также ограничен только одним аргументом, поэтому для сопоставления с несколькими аргументамивам нужно использовать fun a b -> match a, b with....Или вы могли бы просто add принять кортеж напрямую.

Тогда, наконец, вы получите ошибку, потому что вы используете запятую для разделения аргументов функции в add right1, right2, которая, опять же, будет интерпретироваться как кортежвместо.Должно быть add right1 right2.

Окончательная рабочая (или хотя бы компилируемая) функция add имеет вид: 

let rec add : type natural. 
(int, natural) pbtree -> (int, natural) pbtree -> (int, natural) pbtree =
fun a b -> match a, b with
| EmptyTree, EmptyTree -> EmptyTree
| PBTree(left1, value1, right1), PBTree(left2, value2, right2) -> 
PBTree((add left1 left2), value1 + value2, (add right1 right2))
...