haskell - 数据提升语法

Question

我最近发现了 Data.Promotion singletons 的一半.它有大量的类型族，基本上允许在类型级别进行任意计算。我有几个关于使用的问题:

($) 和有什么区别, (%$) , ($$) ，它们是否与 :++$ 相关？ , :.$ ， ETC？这些实际上是中缀运算符吗？我是under the impression所有中缀类型的构造函数都必须以 : 开头.

我正在尝试将构造函数映射到列表上:

{-# LANGUAGE DataKinds, TypeOperators, PolyKinds #-}
import Data.Promotion.Prelude

data Foo a b
type MyList = '[Int, Double, Float]

 -- expects one more argument to `Foo`
type FooList1 b = Map ((Flip Foo) $ b) MyList

-- parse error on the second `b`
type FooList2 b = Map (($ b) :. Foo) MyList 

但我在使用多参数类型构造函数时遇到了麻烦。想法？

我能够用 Data.Promotion 中的等效函数替换我编写的所有类型函数除了这个:

type family ListToConstraint (xs :: [Constraint]) :: Constraint
type instance ListToConstraint '[] = ()
type instance ListToConstraint (x ': xs) = (x, ListToConstraint xs)

Constraint 有什么魔力吗？那种会阻止它作为嵌套对的操作？

Answer 1

正如评论中所解释的，类型级别的中缀函数不再需要以冒号开头的语法要求。所以是的，所有这些都是中缀运算符。没有两个中缀运算符会自动相互关联，但单例库在内部使用一些命名约定，将用于去功能化(见下文)的符号与其正常对应物相关联。

由于类型族不能部分应用，但数据类型可以，这会产生一大堆问题。这就是为什么单例库使用一种称为去功能化的技术:对于每个部分应用的类型函数，它定义一个数据类型。然后有一个(非常大且开放的)类型系列，称为 Apply。它采用所有这些表示部分应用的函数和合适的参数的数据类型并执行实际应用。

类型函数的这种去功能化的表示是

TyFun k1 k2 -> *

出于各种原因(顺便说一句，Richard Eisenberg 的博客文章 "Defunctionalization for the win" 对这一切进行了很好的介绍)，而相应的“正常”类型函数的类型是

k1 -> k2

现在，单例中的所有高阶类型函数都需要去功能化的参数。例如，Map 的种类是

Map :: (TyFun k k1 -> *) -> [k] -> [k1]

并不是

Map :: (k -> k1) -> [k] -> [k1]

现在让我们看看您正在使用的函数:

Flip :: (TyFun k (TyFun k1 k2 -> *) -> *) -> k1 -> k -> k2

第一个参数是一种去功能化的柯里化(Currying)函数 k -> k1 -> k2 , 并将其转换为 k1 -> k -> k2 的普通类型函数.

还:

($) :: (TyFun k1 k -> *) -> k1 -> k

这只是 Apply 的同义词我上面提到过。

现在让我们看看你的例子:

type FooList1 b = Map ((Flip Foo) $ b) MyList  -- fails

这里有两个问题:第一，Foo是数据类型而不是去功能化符号 Flip预计。二、Flip是一个类型族，需要三个参数，但只提供一个。我们可以通过应用 TyCon2 来解决第一个问题。 ，它采用普通数据类型并将其转换为非功能化符号:

TyCon2 :: (k -> k1 -> k2) -> TyFun k (TyFun k1 k2 -> *) -> *

对于第二个问题，我们需要 Flip 的部分应用之一。单例已经为我们定义了:

FlipSym0 :: TyFun (TyFun k1 (TyFun k2 k -> *) -> *)
                  (TyFun k2 (TyFun k1 k -> *) -> *)
            -> *
FlipSym1 ::    (TyFun k1 (TyFun k2 k -> *) -> *)
            -> TyFun k2 (TyFun k1 k -> *) -> *

FlipSym2 ::    (TyFun k1 (TyFun k2 k -> *) -> *)
            -> k2 -> TyFun k1 k -> *

Flip     ::    (TyFun k (TyFun k1 k2 -> *) -> *)
            -> k1 -> k -> k2

如果你仔细看，那么 FlipSymN是 Flip 时所需的表示形式部分应用于 N参数和 Flip对应于假想FlipSym3 .在示例中，Flip应用于一个参数，因此更正的示例变为

type FooList1 b = Map ((FlipSym1 (TyCon2 Foo)) $ b) MyList

这有效:

GHCi> :kind! FooList1 Char
FooList1 Char :: [*]
= '[Foo Int Char, Foo Double Char, Foo Float Char]

第二个例子类似:

type FooList2 b = Map (($ b) :. Foo) MyList

在这里，我们有以下问题:再次，Foo必须使用 TyCon2 将其转换为去功能化符号;运算符部分，例如 $ b在类型级别上不可用，因此会出现解析错误。我们必须使用 Flip再次，但这次FlipSym2 , 因为我们将它应用到运算符 $和 b .哦，然后$部分应用，所以我们需要一个对应于 $ 的符号有 0 个参数。这可用作 $$在单例中(对于符号运算符，去功能化的符号已附加 $ s)。最后，:.也部分应用:它需要三个运算符，但只给出了两个。所以我们从 :.至:.$$$ (三美元，因为一美元对应 0 ，三美元对应 2 )。总而言之:

type FooList2 b = Map ((FlipSym2 ($$) b) :.$$$ TyCon2 Foo) MyList

再一次，这有效:

GHCi> :kind! FooList2 Char
FooList2 Char :: [*]
= '[Foo Int Char, Foo Double Char, Foo Float Char]

我可能是盲人，但我不认为这包含在单例中，这与 Constraint 无关。 s。不过，这是一个有用的功能。它在 library I'm currently working on .不过，它还没有完成，而且大部分都没有记录，这就是我还没有发布它的原因。