GADT頭中的類型變量是否有意義？

這兩個GADT聲明是否有區別？GADT頭中的類型變量是否有意義？

data A a b where 
    ... 

data A :: * -> * -> * where 
    ...

來源

2016-11-24 rightfold

非常好的問題。這是我的寵兒 - 我總是想知道爲什麼我們需要命名索引時，名稱似乎在其他地方不相關。這與在Agda/Coq等依賴系統中使用的歸納類型中的索引與參數非常不同。 – chi

請注意，相反，在類型族中，我們確實在類型族A :: * - > * - > *'和類型族A a :: * - > *'之間存在差異 - 第一個允許例如'A Int Bool = Char; Int Char = Bool「，而後者不是，只允許例如'一個Int =也許'。（儘管在'type family a a * * - > *'中，'a'這個名字仍然是不相關的） – chi

...而'type family B b :: *'不允許你使用例如'MaybeT B a'，這可以通過'type family B :: * - > *'來實現。前者將是[部分類型同義詞應用]（http://stackoverflow.com/a/4923883/745903）。（'LiberalTypeSynonyms'有時可以繞過這個限制。） – leftaroundabout

沒有區別。有人可能會認爲沒有提到的類型變量在頭將需要在構造函數簽名使用它們不同的名稱，如：

data A :: * -> * -> * where 
    AN :: Num x => x -> b -> A x b 
    AS :: IsString s => s -> b -> A s b

然而，隨着the GHC Users Guide說...

與Haskell-98式數據類型聲明不同，data Set a where頭中的類型變量沒有作用域。

...等等這也適用：

data A a b where 
    AN :: Num x => x -> b -> A x b 
    AS :: IsString s => s -> b -> A s b

來源

2016-11-24 13:45:17 duplode

事實上，我最喜歡第一個，但總是最後寫第二個，因爲它更短，我很懶。我認爲它可能有助於文檔給他們帶來令人回味的名字。 – chi

我更喜歡第二種風格，因爲我不喜歡寫類似的簽名。 –

我想它可能會從語法中省略類型變量，但是我們希望部分類型的簽名。 – dfeuer

GADT頭中的類型變量是否有意義？

回答

相關問題