沒有值的GHC TypeLits

試圖設計一個類型驅動的API，我一直試圖得到像下面的工作（使用更復雜的代碼/嘗試，這是剝離到最低限度所需澄清我'我想找）：沒有值的GHC TypeLits

{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE KindSignatures #-} 

module Main where 

import Data.Proxy 
import GHC.TypeLits 

type Printer (s :: Symbol) = IO() 

concrete :: Printer "foo" 
concrete = generic 

generic :: KnownSymbol s => Printer s 
generic = putStrLn (symbolVal (Proxy :: Proxy s)) 

main :: IO() 
main = concrete

這個程序將打印 '富'，但不會：

Could not deduce (KnownSymbol s0) 
    arising from the ambiguity check for ‘generic’ 
from the context (KnownSymbol s) 
    bound by the type signature for 
      generic :: KnownSymbol s => Printer s 
    at test5.hs:14:12-37 
The type variable ‘s0’ is ambiguous 
In the ambiguity check for: 
    forall (s :: Symbol). KnownSymbol s => Printer s 
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes 
In the type signature for ‘generic’: 
    generic :: KnownSymbol s => Printer s

啓用AllowAmbiguousTypes沒有真正的幫助。任何方式來讓這個工作無論如何？

來源

2015-02-17 Nicolas Trangez

你應該提供參數在具體的調用網站？ – 2015-02-17 22:15:53

@PeterK這是可能的，是的，但我不明白這是怎麼改變的？ – 2015-02-17 22:29:36

「Printer」foo「'與'Printer」bar「'是完全相同的類型，因爲它們都是'IO（）'的類型同義詞，所以它不能以當前形式工作。 – 2015-02-17 22:30:11

類型同義詞（用type定義）在類型查詢期間替換爲它們的定義。問題是，Printer在其定義中沒有提及s，這導致了以下的限制：

generic :: KnonwSymbol s => IO()

這種類型的簽名不具有=>的s權等失敗的模糊性檢查。它不能真正起作用，因爲在使用它時無處指定s應該是什麼。

不幸的是，GHC在錯誤消息中表示類型同義詞的方式不一致。有時它們會擴大，有時會被保留下來。具有諷刺意味的是，我認爲錯誤信息的改進使得這個特定的錯誤難以追蹤：通常，根據您定義的類型表達錯誤更加清晰，但這裏隱藏了歧義的原因。

您需要的是提供不依賴於類型同義詞的相關類型級別符號的某種方法。但首先，您需要啓用ScopedTypeVariables並將forall添加到generic的簽名中，以確保類型簽名中的s和Proxy :: Proxy s中的s是相同的。

有兩種可能性：

變化Printer爲newtype，當你使用它解開它：

newtype Printer (s :: Symbol) = Printer { runPrinter :: IO() } 

generic :: forall s. KnownSymbol s => Printer s 
generic = Printer $ putStrLn (symbolVal (Proxy :: Proxy s)) 

main = runPrinter generic

傳遞一個額外的Proxy參數generic，就像symbolVal：
```
concrete :: Printer "foo" 
concrete = generic (Proxy :: Proxy "foo") 

generic :: forall proxy s. KnownSymbol s => proxy s -> IO() 
generic _ = putStrLn (symbolVal (Proxy :: Proxy s)) 
```
proxy作爲一個類型變量是一個整潔的習慣用法，它可以讓你不依賴於Data.Proxy，並讓呼叫者代替他們想要的任何東西。

來源

2015-02-17 22:27:19

謝謝。回想起來，使用簡單類型同義詞時，「幻影」參數顯得非常明顯。 – 2015-02-20 13:55:05

這是錯誤的：

generic :: KnownSymbol s => Printer s 
generic = ...(Proxy :: Proxy s)

最後s無關與s它上面。與頂級類型註釋一樣，它在本地隱含地被普遍量化。該代碼實際上意味着

generic :: KnownSymbol s => Printer s 
generic = ...(Proxy :: forall z. Proxy z)

要解決上面，使ScopedTypeVariables和使用

-- the explicit forall makes s available below 
generic :: forall s. KnownSymbol s => Printer s 
generic = ...(Proxy :: Proxy s)

還有其他的問題，不過，因爲吉洪Jelvis在他的回答指出。

來源

2015-02-17 22:25:07 chi

'ScopedTypeVariables'是必要的，但不夠：代碼的歧義檢查仍然失敗，即使有適當的範圍。 – 2015-02-17 22:27:59

沒有值的GHC TypeLits

回答

相關問題