当我们无论如何都可以绕过限制时，为什么不能部分应用类型族/同义词？

Question

考虑以下

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 

一切都很好。

在我看来，我已经颠覆了“不能部分应用类型同义词”的事情。这种转变看起来很混乱，但它也是机械的，我不清楚这种转变在什么情况下不起作用？

然后我问，不能部分应用类型同义词/家族的限制的目的是什么，如果可以通过将您的同义词移动到类型家族中来解决它？

Answer 1

答案是因为。只是因为。