瞭解類型族

我在學習類型族並試圖理解爲什麼我沒有在特定情況下得到編譯時錯誤。瞭解類型族

我的家庭類型的定義如下：

type family Typ a b :: Constraint 
type instance Typ (Label x) (Label y) =()

我有如下兩個功能：

func1 :: (Typ (Label "la") (Label "lb")) => Label "la" -> Label "lb" -> String 
func1 = undefined 

func2 :: (Typ (Label "la") String) => Label "la" -> String -> String 
func2 = undefined

這兩個函數編譯OK。

當我嘗試查看func1的類型時，我得到正確的簽名。但是，當我嘗試查看func2的類型，我得到的錯誤以下錯誤

無法推斷（典型值（標籤「LA」）字符串）

爲什麼會這樣呢？有人能幫助我理解嗎？

來源

2015-08-25 Prasanna K Rao

我的假設是，這是因爲有一個實例爲'Typ（Label x）（Label y）'聲明，但不是'Typ（Label x）String'。「Label」的定義是什麼？ – ryachza

'數據標籤（l :: Symbol）= Get'我希望爲'func2'獲得編譯時錯誤，而不是運行時錯誤 –

您可能對[關於上下文減少的討論]感興趣（https：/ /www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-910004.5.3）。我很想把它稱爲ghci抱怨的一個錯誤：它可能不應該在用戶提供的類型簽名上減少上下文。請注意，當然，如果您曾嘗試在真正的程序中使用'func2'，它最終會追溯到沒有上下文的'main'，並且特別不允許具有'Typ（Label「la」）在其上下文中的字符串 - 你會得到一個類型錯誤。 –

我可以複製你這個定義的Label描述了：

import GHC.TypeLits (Symbol) 

data Label (a :: Symbol)

並添加：

type instance Typ (Label x) String =()

然後提供func2

類型編輯

對不起，我誤解了這個問題。我的理解是，檢查約束的可滿足性將被推遲到實際使用func2，因爲稍後可以添加實例。

例如，增加：

func3 = func2 (undefined :: Label "la") ""

使其在編譯時失敗。

我理解它的方式是，func2是說，如果你給我一個Label "la"和String和Typ (Label "la") String一個實例是在範圍上的時候，我給你一個String。但是func2不需要知道範圍內的實例如果它有一個，它將如何處理。

來源

2015-08-25 22:06:21 ryachza

是的@DanielWagner。你的理解是正確的。我對爲什麼類型錯誤被延遲感興趣。 –

@PrasannaKRao「爲什麼會延遲」 - 這部分很簡單。這是一個普遍的原則，即對不滿意約束的抱怨盡可能延遲，以支持單獨編譯。（通過單獨的編譯，你可能不知道所有的方法來滿足約束。）但我不確定「沒有更遠」的部分。 –

@PrasannaKRao對不起，我最初誤解並更新了我的答案。 – ryachza

回答

相關問題