Tại sao mã này không vi phạm "yêu cầu bão hòa của các họ loại"?

Question

Tôi có ví dụ này tối thiểu làm việc (chọn lọc từ thư viện singletons) của ánh xạ một gia đình kiểu trên một danh sách loại cấp:

{-# 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  

Có vẻ như để làm việc:

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

Mã này được giải thích trong bài đăng Defunctionalization for the win. Đó là một giải pháp cho thực tế là "GHC sẽ không cho phép một biến kiểu hợp nhất với một họ loại". Điều này được gọi là "yêu cầu bão hòa của các loại gia đình".

Nghi ngờ của tôi là: khi chúng tôi "chạy" :kind! Map (TyCon1 Flip) '[Char,Int] có vẻ như, trong dòng type instance Apply (TyCon1 f) x = f x, f sẽ được khớp với gia đình loại Flip của chúng tôi. Tại sao điều này không vi phạm yêu cầu bão hòa?

Answer 1

Tôi đang trả lời câu hỏi của riêng mình với thông tin được chọn lọc từ nhận xét của người gửi và nhận xét của người dùng2407038.

Hóa ra mã của tôi đã làm vi phạm yêu cầu bão hòa. Tôi không tìm thấy lỗi vì một hành vi lạ (lỗi?) Của :kind! trong ghci. Nhưng hãy viết loại trong chính tệp hs cho lỗi biên dịch.

TyCon1 không dành cho các họ loại, nhưng đối với việc đóng gói các nhà xây dựng kiểu thông thường như Maybe, không có vấn đề gì hợp nhất với các biến kiểu. Ví dụ: type Foo = Map (TyCon1 Maybe) '[Char,Int] hoạt động tốt.

Đối với các họ loại, chúng tôi cần xác định loại phụ trợ đặc biệt cho từng loại, sau đó xác định một thể hiện Apply cho loại. Như thế này:

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

type Boo = Map FlipSym '[Char,Int] 

Lưu ý rằng cách này loại gia đình Flip không thống nhất với bất kỳ loại biến nào.