Bu kod neden "tip ailelerin doygunluk gereksinimini" ihlal etmiyor?

Question

Bir tür düzeyinde liste üzerinde bir tür ailesini haritalama (singletons kütüphanesinden itlaf) bu asgari çalışma örneği vardır:

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

kod açıklanmıştır:

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

İşe görünüyor Defunctionalization for the win numaralı yazıda. “GHC, bir tip değişkenin tür ailesiyle birleşmesine izin vermeyeceği” için bir çözümdür. Buna "tip ailelerin doyma gereksinimi" denir.

Benim şüphe: Biz :kind! Map (TyCon1 Flip) '[Char,Int] "koşmak" zaman çizgisi type instance Apply (TyCon1 f) x = f x yılında, f bizim Flip tipi ailesi ile uyumlu olacak, gibi görünüyor. Bu neden doygunluk şartını ihlal etmiyor?

Answer 1

Kendi sorumu dfeuer ve user2407038'in yorumlarından silen bilgilerle yanıtlıyorum.

kodumun kodunun doygunluk gereksinimini ihlal ettiğini öğrenir. Ben ghci içinde :kind! tuhaf bir davranış (hata?) Nedeniyle hata bulamadık. Ancak, hs dosyasındaki dosyanın yazılması, bir derleme hatası verir.

TyCon1, tür aileler için değil, tip değişkenleriyle birleştirmede sorun yaşanmayan Maybe gibi düzenli tür kurucular için sarılır. Örneğin, type Foo = Map (TyCon1 Maybe) '[Char,Int] iyi çalışıyor.

Türü aileler için, her biri için özel bir yardımcı tür tanımlamalı ve ardından tür için bir Apply örneği tanımlamalıyız. Şunun gibi:

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

type Boo = Map FlipSym '[Char,Int] 

Bildirim o Flip tipi ailesi her tür değişkenle birleştirici değil bu şekilde.