爲什麼這段代碼不會侵犯「類型族的飽和要求」？

我有過一個類型級列表映射類型的家庭這個最小的工作示例（從singletons庫撲殺）：爲什麼這段代碼不會侵犯「類型族的飽和要求」？

{-# language PolyKinds #-} 
{-# language DataKinds #-} 
{-# language TypeFamilies #-} 
{-# language TypeOperators #-} 

data TyFun :: * -> * -> * 

data TyCon1 :: (k1 -> k2) -> (TyFun k1 k2 -> *) 

type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2 
type instance Apply (TyCon1 f) x = f x 

type family Map (f :: TyFun a b -> *) (as :: [a]) :: [b] where 
    Map f '[] = '[] 
    Map f (x ': xs) = Apply f x ': Map f xs 

type family Flip t :: * where 
    Flip Int = Char 
    Flip Char = Int

看來工作：

ghci> :set -XDataKinds 
ghci> :kind! Map (TyCon1 Flip) '[Char,Int] 
Map (TyCon1 Flip) '[Char,Int] :: [*] 
= '[Int, Char]

的代碼解釋在帖子Defunctionalization for the win。對於「GHC不會讓一個類型變量與一個類型系列相結合」這一事實，這是一個解決方法。這被稱爲「類型族的飽和要求」。

我的疑問是：當我們「跑」:kind! Map (TyCon1 Flip) '[Char,Int]看來，在線type instance Apply (TyCon1 f) x = f x,f將與我們的Flip類型家庭匹配。爲什麼這不符合飽和要求？

來源

2016-11-23 danidiaz

我不認爲這應該工作。然而，這是完全無害的，因爲類型檢查中擴展了同義詞。 – dfeuer

我相信你真的應該爲自己的'Apply'實例提供'Flip'的defunctionalization符號。 'TyCon1'旨在應用於類型構造函數。順便說一下，這是什麼版本的GHC？ – dfeuer

@dfeuer我正在使用GHC 8.0.1。顯然，這個東西在ghci中使用'：kind！'時會起作用，但是如果我嘗試在腳本中添加類似Boo = Map（TyCon1 Flip）'[Char，Int]'的東西，它會給我一個編譯錯誤。 – danidiaz

我回答自己的問題，從dfeuer和user2407038的評論中挑選信息。

原來，我的代碼做了侵犯了飽和要求。我沒有發現錯誤，因爲在ghci中有一個奇怪的行爲（bug？）:kind!。但是在hs文件本身中寫入類型會產生編譯錯誤。

TyCon1不適用於類型族，而是用於包裝常規類型的構造函數，如Maybe，它們沒有與類型變量統一的問題。例如，type Foo = Map (TyCon1 Maybe) '[Char,Int]正常工作。

對於類型族，我們需要爲它們中的每一個定義一個特殊的輔助類型，然後爲該類型定義一個Apply實例。就像這樣：

data FlipSym :: TyFun * * -> * 
type instance Apply FlipSym x = Flip x 

type Boo = Map FlipSym '[Char,Int]

注意，這種方式Flip類型的家庭是不與任何類型的變量統一。

來源

2016-11-24 20:57:08 danidiaz

對不起，我沒有得到自己答覆。你至少和我寫的一樣好。我想挑選一個尼克特：我不喜歡那個家族的名字叫Flip。在我看來，這個名字總是被定義爲'newtype Flip（f :: j - > k - > *）（y :: k）（x :: j）= Flip {unFlip :: f x y}'。產生的「flip」類型級版本經常出現，並且通常在類型同義詞版本（'type Flip f x x = f x y'）不起作用的上下文中。 – dfeuer

爲什麼這段代碼不會侵犯「類型族的飽和要求」？

回答

相關問題