0

我正在尝试编写两个相互归纳数据类型的声明，它们都将类型参数作为参数，如下所示：

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 行是包含“type foo 'a”的行）

这个错误是什么意思，我能做些什么来解决它？

如果我删除类型参数（例如，给 foo.x 提供 int 类型），我就不会再收到错误了。同样，如果我只给其中一种类型一个类型参数而不给另一个类型，我也没有错误。

4

1 回答 1

2

在这种情况下，F* 无法推断出宇宙。但是，您可以提供显式的 Universe 实例化。例如，以下是三种可能的解决方案：

首先，一个双宇宙多态的，最通用但也可能使用起来很麻烦

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

一个单一的宇宙多态解决方案，虽然不太通用，但可能更简单一些：

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
于 2020-01-27T19:08:24.233 回答