私はタイプレベルのリスト上のタイプの家族をマッピングする(singletonsライブラリから抜粋)この最小限の作業例を持っています。なぜこのコードは「型ファミリの飽和要件」に違反しないのですか?
ghci> :set -XDataKinds
ghci> :kind! Map (TyCon1 Flip) '[Char,Int]
Map (TyCon1 Flip) '[Char,Int] :: [*]
= '[Int, Char]
コードを説明します
{-# 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
動作するようです投稿の中でDefunctionalization for the win。これは、 "GHCは型変数を型族と統一させません"という事実を回避する方法です。これは「タイプファミリの飽和要件」と呼ばれます。
私の疑いがある:私たち「実行」:kind! Map (TyCon1 Flip) '[Char,Int]
ラインtype instance Apply (TyCon1 f) x = f x
で、f
は、私たちのFlip
型家族と照合されます、と思われるとき。なぜこれは飽和要件を侵害しないのですか?
私はそれが動作するとは思わない。しかし、類義語は型チェックの際に拡張されるので完全に無害です。 – dfeuer
私はあなたが本当に 'Flip'のために' apply'インスタンスを使って機能停止シンボルを提供することになっていると思います。 'TyCon1'は型コンストラクタに適用されることを意図しています。ところで、これはGHCのどのバージョンですか? – dfeuer
@dfeuer GHC 8.0.1を使用しています。どうやら、ghciで ':kind! 'を使ったときに動作するようですが、' Boo = Map(TyCon1 Flip)' [Char、Int] 'のようなものをスクリプトに追加しようとすると、コンパイルエラーが出ます。 – danidiaz