修复语言环境扩展中的类型变量 [英] Fixing type variables in locale extensions

问题描述

给定这个代码

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

所以似乎 Isabelle 不明白 baz 和 foo 应该是同一类型.有没有办法解决这个问题?

so it seems that Isabelle does not understand that baz and foo should be of the same type. Is there a way to fix this?

推荐答案

问题在于您声明的区域设置 B 和 C.B 的声明等价于以下

The problem is with your declaration of locales B and C. The declaration for B is equivalent to the following

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

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

Locales imports only remember the names of the parameters, but not the names of type variables. Thus, as you have not specified the type for foo, the most general type for B's parameter is the following:

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

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

You can see this using the command print_locale B. The same happens in the declaration of locale C.

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

If you want to have the same type for foo and bar, you have to make the connection explicit in the locale declarations. There are two ways to do this.

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

和

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

这篇关于修复语言环境扩展中的类型变量的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！