型家庭，GADTs並命名爲記錄

在下面的代碼編譯錯誤，T1和T2編譯罰款，但T3失敗：型家庭，GADTs並命名爲記錄

{-# LANGUAGE GADTs #-} 
{-# LANGUAGE TypeFamilies #-} 

type family F a 

data T1 b where 
    T1 :: a -> T1 (F a) 

data T2 b where 
    T2 :: { x2 :: a } -> T2 a 

data T3 b where 
    T3 :: { x3 :: a } -> T3 (F a)

我試圖理解爲什麼。 T3只是T1但帶有一個已命名的記錄。這似乎沒有那麼特別，因爲可以使用構造函數語法來提取它。

這些例子可能看起來很愚蠢，但在我的代碼中有a的限制，例如， (Show a)，所以這些值可以在提取時使用。

來源

2017-01-31 Clinton

讓我們忘記T2和T3，並試圖爲T1定義提取函數。該類型應該是什麼？你可能猜到x1 :: T1 (F a) -> a。但是，這是不對的，如果你嘗試它，那麼你會得到定義T3的同樣的錯誤。

的問題是，如果有人給你一個T1 T，你碰巧知道一個類型A這樣F A是T，則不能得出這樣的結論T1 T包含A類型的值，因爲它可能代替含有另一種類型B與F B等於T。作爲一個極端的例子，假設我們有

type instance F _ =()

那麼，如果我們把我們的猜測x1 :: T1 (F a) -> a，我們不得不

T1 :: a -> T1() 
x1 :: T1() -> b

和作曲這些將讓我們寫a -> b，這是不好的。

真正的類型x1是一樣的東西存在，提供約束

T1 t -> (exists a. (F a ~ t) *> a)

這GHC不支持。

與T3的問題是有效的，如果你有

data T3' where T3' :: { x3' :: a } -> T3'

可以提取與模式匹配字段（如果有多個字段或約束，這可能是有用的）相同，但與記錄選擇器或功能。

來源

2017-01-31 14:06:06

型家庭，GADTs並命名爲記錄

回答

相關問題