定影型變量

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" 

區域設置進口只記得參數的名稱，而不是類型變量的名稱。因此，當你沒有指定類型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"