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

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

类型族不能部分应用，因为它会破坏类型推断。在 GHC 中，等价f a ~ g b于f ~ g和a ~ b。f如果和g被允许成为类型家族，情况就不再是这样了。您可以通过区分两种类型级别应用程序来解决这个问题，但用例可能不像现在引入类型系列时那么清晰。另请参阅Haskell 中的高阶类型级编程。

这种围绕缺乏部分应用的转变称为去功能化。

• 这篇文章讨论了它在单例中的使用。
• 它曾经是一种编译函数式程序的技术，但它通常对于直接编程很有用。在这里查看更多内容。