Ограничение типа записи для полиморфных вариантов с параметрами универсального типа - PullRequest
1 голос
/ 24 апреля 2019

Справочная информация: я пытался создать что-то, как описано в статье, Тип данных по меню - но пытался выяснить, могут ли полиморфные варианты OCaml привести к чистой реализации ReasonML.

Мой код приведен в синтаксисе ReasonML, но вопрос в равной степени применим к OCaml.

Я начну с определения двух модулей для Val и Add, каждый из которых реализует fmap - делая ихфунктор в стиле Хаскеля.

module type Functor = {
  type t('a);
  let fmap: ('a => 'b, t('a)) => t('b);
};

module Val = {
  type t('e) = [ | `Val(int)];
  let fmap = _ =>
    fun
    | `Val(x) => `Val(x);
};

module Add = {
  type t('e) = [ | `Add('e, 'e) ];

  let fmap = f =>
    fun
    | `Add(x, y) => `Add((f(x), f(y)))
};

Я могу довольно легко создать тип данных Algebra, который объединяет эти два модуля в один, с очень простой реализацией fmap.

module Algebra = {
  type t('t) = [ Val.t('t) | Add.t('t)];

  let fmap = (f, x) =>
    switch (x) {
    | #Val.t as v => Val.fmap(f, v)
    | #Add.t as o => Add.fmap(f, o)
    };
};

Это компилирует и работает в более широком контексте, где я могу оценить выражение, состоящее как из значений Val, так и Add.

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

Моя первая попытка такая:

module JoinAlgebra = (A1: Functor, A2: Functor) => {
  type t('t) = [ A1.t('t) | A2.t('t)];

  let fmap = (f, x) =>
    switch (x) {
    | #A1.t as v => Val.fmap(f, v)
    | #A2.t as o => Add.fmap(f, o)
    };
};

Но это не работает.Поскольку A1.t и A2.t могут быть чем угодно, я не могу объединить их как полиморфный вариант.

Ошибка: тип A1.t ('t) не является полиморфным вариантом типа

Я попытался добавить ограничение типа к типу модуля Functor:

module type Functor = {
  type t('a) = 'a constraint [> ] = 'a;
  let fmap: ('a => 'b, t('a)) => t('b);
};

module JoinAlgebra = (A1: Functor, A2: Functor) => {
  type t('t) = [ A1.t('t) | A2.t('t)]; // This line fails
}

Теперь я получаю ошибку компилятора

Ошибка: тип A1.t ([>]) не является полиморфным вариантом типа

Можно ли как-нибудь создать модуль-функтор, автоматически основанный на двух модулях?

Примечание о версиях OCaml : здесь я использую bucklescript v. 5, который использует компилятор OCaml 4.02.Но решения, которые требуют 4.06, также приветствуются (поддержка должна прийти в Bucklescript)

1 Ответ

2 голосов
/ 25 апреля 2019

Ваша Functor подпись определяет абстрактный тип 'a t. Как вы правильно заметили, «поскольку A1.t и A2.t могут быть чем угодно, я не могу объединить их как полиморфный вариант». Чтобы решить проблему, заключающуюся в том, что 'a t в Functor является абстрактным, попробуйте сделать его полиморфным, выполнив:

module Functor = struct
  type 'a t = 'a constraint 'a = [< ]
end

Однако переменная типа 'a больше не обозначает обернутое значение, а скорее полиморфное ограничение варианта. Это, конечно, не то, что вы хотите. Вы получаете ошибку Error: The type A1.t([> ]) is not a polymorphic variant type, потому что вы можете заменить только "точные типы вариантов" на полиморфные варианты:

Первый случай - это точный тип варианта: известны все возможные теги со связанными с ними типами, и все они могут присутствовать. Его структура полностью известна.

...

Во всех трех случаях теги могут быть либо указаны непосредственно в форме `tag-name [of typexpr], либо косвенно через выражение типа, которое должно быть расширено до точного варианта типа, спецификации тега которого вставлены вместо него. .

(https://caml.inria.fr/pub/docs/manual-ocaml/types.html#polymorphic-variant-type)

Вам не нужны полиморфные варианты для JoinAlgebra. Просто сделай:

module JoinAlgebra (A1 : Functor) (A2 : Functor) = struct
  type 't t = Left of 't A1.t | Right of 't A2.t

  let fmap f x =
    match x with
    | Left v -> Left (A1.fmap f v)
    | Right o -> Right (A2.fmap f o)
end

Преимущество состоит в том, что 'a t в Functor остается абстрактным, а код работает для Functor модулей, которые не определяют полиморфные варианты.

...