haskell 为什么不能部分地应用类型族/同义词,而我们却可以绕过这个限制呢?

velaa5lx  于 2023-04-12  发布在  其他
关注(0)|答案(1)|浏览(126)

考虑以下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

一切都很好。
在我看来,我已经颠覆了“不能部分应用类型同义词”的概念。这种转换看起来很混乱,但它也很机械,而且对我来说,这种转换在什么情况下不起作用并不明显?
那么我问,如果可以通过将同义词移到类型族中来解决它,那么不能部分应用类型同义词/族的限制的目的是什么?

rjee0c15

rjee0c151#

类型族不能部分应用,因为它破坏了类型推断。在GHC中,相等f a ~ g b等效于f ~ ga ~ b。如果允许fg作为类型族,则不再是这种情况。您可以通过区分两种类型级别的应用程序来解决此问题,但是在引入类型家族的时候,用例可能并不像现在这样清晰。
解决部分应用缺乏的转换称为去功能化。

  • This post讨论了它在单例中的使用。
  • 它曾经是一种用于编译函数式程序的技术,但它通常用于直接编程。查看更多here

相关问题