考虑以下Map
类型函数:
type Map :: (k1 -> k2) -> [k1] -> [k2]
type family Map f l where
Map _ '[] = '[]
Map f (x : xs) = f x : Map f xs
然后我可以定义:
type MkPair a = (a, a)
并尝试执行以下操作:
type Blah = Map MkPair [Int, Char]
但我发现类型同义词不能部分应用。
但我可以做这个稍微迂回的路线:
type Mapper :: k1 -> k2 -> Type
data Mapper k1 k2 where
Mapper :: Type -> Mapper k1 k2
type MapF :: Mapper k1 k2 -> [k1] -> [k2]
type family MapF f l where
MapF _ '[] = '[]
MapF ft (x : xs) = MapFT ft x : MapF ft xs
type MapFT :: Mapper k1 k2 -> k1 -> k2
type family MapFT kt k1
data MkPair
type instance MapFT ('Mapper MkPair :: Mapper Type Type) a = (a, a)
type Blah = MapF ('Mapper MkPair :: Mapper Type Type) [Int, Char]
-- This compiles
f :: Proxy Blah -> Proxy '[(Int, Int), (Char, Char)]
f = id
我甚至可以这样做:
data SymMap
type instance MapFT ('Mapper SymMap :: Mapper Symbol Type) a = Proxy a
g :: Proxy (MapF ('Mapper SymMap :: Mapper Symbol Type) ["hello", "world"]) -> Proxy '[Proxy "hello", Proxy "world"]
g = id
一切都很好。
在我看来,我已经颠覆了“不能部分应用类型同义词”的概念。这种转换看起来很混乱,但它也很机械,而且对我来说,这种转换在什么情况下不起作用并不明显?
那么我问,如果可以通过将同义词移到类型族中来解决它,那么不能部分应用类型同义词/族的限制的目的是什么?
1条答案
按热度按时间rjee0c151#
类型族不能部分应用,因为它破坏了类型推断。在GHC中,相等
f a ~ g b
等效于f ~ g
和a ~ b
。如果允许f
和g
作为类型族,则不再是这种情况。您可以通过区分两种类型级别的应用程序来解决此问题,但是在引入类型家族的时候,用例可能并不像现在这样清晰。解决部分应用缺乏的转换称为去功能化。