我有这个将类型族映射到类型级列表的最小工作示例(从 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
匹配类型家庭。为什么这不违反饱和要求?
最佳答案
我正在用从 dfeuer 和 user2407038 的评论中挑选出来的信息来回答我自己的问题。
原来我的代码确实违反了饱和度要求。由于 :kind!
的奇怪行为(错误?),我没有找到错误。在 ghci 中。但是在 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
类型族不与任何类型变量统一。
关于haskell - 为什么这段代码不侵犯 "saturation requirement of type families"?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/40758738/