Взаимно индуктивные типы данных с параметрами типа - PullRequest
Новая
       6

Взаимно индуктивные типы данных с параметрами типа

0 голосов
/ 27 января 2020

Я пытаюсь написать объявление двух взаимно индуктивных типов данных, которые оба принимают параметр типа в качестве аргументов следующим образом: 

noeq
type foo 'a =
    | FooA: x: 'a -> foo 'a
    | Foob: y: bar 'a -> foo 'a
and bar 'b =
    | BarA: x: int -> bar 'b
    | BarF: y: foo 'b -> bar 'b

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

LabeledStates.fst (59,0-64,31): (Ошибка 67) Не удалось разрешить неравенства юниверсов для индуктивов. Об ошибке 1 (см. Выше)

(где строка 59 - строка, включающая тип) foo 'a ")

Что означает эта ошибка и что я могу сделать, чтобы исправить ее?

Если я удаляю параметры типа (и, например, присваиваю foo.x тип int ) Я больше не получаю ошибок. Точно так же, если я просто даю одному из типов параметр типа, но не другой, у меня также нет ошибок.

1 Ответ

2 голосов
/ 27 января 2020

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

Во-первых, полиморф с двойной вселенной c один, наиболее общий, но, возможно, довольно громоздкий для использования 

noeq
type foo (a:Type u#a) : Type u#(max a b) =
   | FooA: x: a -> foo a
   | Foob: y: bar u#b u#a a -> foo a
and bar (b:Type u#b) : Type u#(max a b) =
   | BarA: x: int -> bar b
   | BarF: y: foo u#b u#a b -> bar b

полиморф с одиночной вселенной c решение, возможно, немного более простое, хотя и менее общее: 

noeq
type foo1 (a:Type u#a) : Type u#a =
   | Foo1A: x: a -> foo1 a
   | Foo1b: y: bar1 u#a a -> foo1 a
and bar1 (b:Type u#a) : Type u#a =
   | Bar1A: x: int -> bar1 b
   | Bar1F: y: foo1 u#a b -> bar1 b

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

noeq
type foo0 (a:Type u#0) : Type u#0 =
   | Foo0A: x: a -> foo0 a
   | Foo0b: y: bar0 a -> foo0 a
and bar0 (b:Type u#0) : Type u#0 =
   | Bar0A: x: int -> bar0 b
   | Bar0F: y: foo0 b -> bar0 b
...