類型的數字簽名和類型的家庭

我希望類型的數字簽名和類型的家庭

type family Rep a

和

type family Rep :: * -> *

是相同的，但它似乎是有區別的

type family Rep a 
type instance Rep Int = Char 
-- ok 

type family Rep :: * -> * 
type instance Rep Int = Char 
-- Expected kind * -> *, but got 'Int' instead

難道我只是絆了一Haskell擴展的bug，還是有一些點這種行爲？

來源

2017-07-31 hgiesel

重點是類型族不是'類型級函數'。他們是'家庭的類型'。您應該將值級別模式匹配和類型族實例聲明之間的語法相似性視爲重合 - 它們具有完全不同的語義（例如，嘗試編寫與構造函數'Left :: a - >或任何ab匹配的值級函數'）。你已經目睹了這個差異的最小例子。第二類家庭基本上只是一個類型的同義詞，因爲它只能有一個實例。第一個是一個適當的類型家庭。 – user2407038

我希望我有一個簡單的方法來解釋「類型級函數」和「類型家族」之間的區別，但我沒有。不同之處在於，第一類家庭不能部分應用（當然，第二類也是不可能的，但第二類的使用是飽和應用，因爲它需要0個參數） - 換句話說，第一類家族沒有一種可以在Haskell類型系統中分配給它的類型。 – user2407038

是的，存在細微差別。

粗略地說，type family F a :: *->*指出，比如說，F Int就像[]，Maybe的射類型構造。這是由編譯器，它可以輸入檢查以下內容代碼利用：

type family F a :: * -> * 

-- these three examples can be removed/changed, if wished 
type instance F Int = [] 
type instance F Char = Maybe 
type instance F Bool = (,) String 

foo :: (F Int a :~: F Int b) -> (a :~: b) 
foo Refl = Refl

要鍵入檢查以上，編譯器利用的是 F Int a ~ F Int b意味着a ~ b，從注入下面的事實。

相反，聲明type family F a b :: *不能保證F Int的注入性，因爲以下內容變得合法。

type family F a b :: * 
type instance F Int a =()

來源

2017-07-31 23:20:55 chi

類型的數字簽名和類型的家庭

回答

相關問題