在存在時包裝類型類型函數時模糊類型變量

我在解釋器中使用類型無標籤最終編碼。不幸的是，我遇到了類型檢查階段的問題。最小測試用例如下：在存在時包裝類型類型函數時模糊類型變量

{-# LANGUAGE RankNTypes, ExistentialQuantification, NoMonomorphismRestriction #-} 
class Program repr where 
    ... 
    intro1 :: repr a (a,()) 
    ... 

data DynTerm repr = forall x y. (Typeable x, Typeable y) => DynTerm (repr x y) 

ghci> DynTerm intro1

這將產生以下的錯誤：

Could not deduce (Typeable x0) arising from a use of `DynTerm' 
from the context (Program repr) 
    bound by the inferred type of it :: Program repr => DynTerm repr 
    at <interactive>:3:1-14 
The type variable `x0' is ambiguous 
Possible fix: add a type signature that fixes these type variable(s) 
Note: there are several potential instances: 
    instance Typeable Void -- Defined in `Data.Void' 
    instance [overlap ok] Typeable() 
    -- Defined in `Data.Typeable.Internal' 
    instance [overlap ok] Typeable Bool 
    -- Defined in `Data.Typeable.Internal' 
    ...plus 25 others 
In the expression: DynTerm intro1 
In an equation for `it': it = DynTerm intro1

我預期編譯器原因如下：

嘗試與x到一個統一。
將Typeable a添加到約束列表（我可以通過類型註釋手動添加它，這沒有什麼區別）。
成功。
嘗試使用y統一（a，（））。
請注意，由於我們假設了Typeable a，Typeable（a，（））也成立。
成功。

但是，它似乎沒有統一x。

來源

2014-02-12 klkblake

當構建使用DynTerm構造類型DynTerm的值，GHC已經知道具體的類型，以決定哪些Typeable字典應該在包裝x和y。在您的測試表現，你是不是提供足夠的類型信息以確定具體的類型，因此你會得到某些類型變量不明確的錯誤。如果您專門選擇一種具體的Typeable類型，它會起作用。

實施例（與ScopedTypeVariables）：

test :: forall repr. Program repr => DynTerm repr 
test = DynTerm (intro1 :: repr Int (Int,()))

來源

2014-02-12 10:36:49 kosmikus

啊，這是有道理的。你知道是否有辦法避免類型具體的要求？在代碼中的這一點上，我實際上並不知道a的最終類型是什麼。 – klkblake

我不明白你的後續問題。你真的想用這個做什麼？ – kosmikus

它是解釋器的一部分，特別是從無類型表達式轉換爲鍵入表達式。「repr a b」代表從a到b的函數（repr部分是用於我正在使用的TTF編碼）。問題是當我轉換多態函數的主體時，沒有有效的具體類型。我有點希望GHC能夠跟蹤部分詞典，最後把整個程序轉換成適當的類型，並讓GHC填充空洞。這就是說，我只記得演員是用unsafeCoerce實施的，所以這不可能奏效。 – klkblake

如kosmikus指出，ExistentialQuantification意味着你將抽象的過度型變量，但你的數據類型的實現者必須選擇一個單一的，單態類型：

When a value of this type is constructed, s will be instantiated to some concrete type. When such a value is analysed, s is abstract.

考慮以下幾點：

data D = forall a . Show a => D (a -> String) 
-- test0 = D show -- Invalid! 
test1 = D (show ::() -> String) 

data E = E (forall a . Show a => a -> String) 
test2 = E show -- Invalid! 
-- test3 = E (show ::() -> String)

因此，也許你想

data DynTerm repr = DynTerm (forall x y. (Typeable x, Typeable y) => repr x y)

但是，這仍然不能與intro1工作 - 它不夠多態（(a,())比x更具體）。如果你有intro2 :: Program repr => repr x y，你可以寫DynTerm intro2。

來源

2014-02-12 11:36:55 user2407038

在存在時包裝類型類型函數時模糊類型變量

回答

相關問題