polymorphism - 修复语言环境扩展中的类型变量

Question

给定这段代码

locale A =
  fixes foo :: "'a"

locale B = A +
  fixes bar :: "'a × 'a"

locale C' = A +
  fixes baz :: "'a"
begin
  sublocale B foo "(foo, baz)".
end

我明白了

Type unification failed

Failed to meet type constraint:

Term:  (foo, baz) :: 'b × 'a
Type:  'b × 'b

看来伊莎贝尔不明白baz 和foo 应该是同一类型。有办法解决这个问题吗？

Answer 1

问题出在您对区域设置 B 和 C 的声明上。 B 的声明等同于以下内容

locale B = A foo for foo +
  fixes bar :: "'a * 'a"

Locales 导入只记住参数的名称，而不是类型变量的名称。因此，由于您没有指定 foo 的类型，B 的参数最通用的类​​型如下:

 foo :: 'b
 bar :: 'a * 'a

您可以使用命令 print_locale B 看到这一点。同样的情况也发生在语言环境 C 的声明中。

如果您希望foo 和bar 具有相同的类型，则必须在语言环境声明中显式连接。有两种方法可以做到这一点。

locale B = A foo
  for foo :: 'a
  +
  fixes bar :: "'a * 'a"

和

locale B = A +
  constrains foo :: 'a
  fixes bar :: "'a * 'a"