数据提升语法

Question

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

1. 有什么区别 ($), (%$), ($$), ，它们与 :++$, :.$, ， ETC？这些实际上是中缀运算符吗？我曾是 在这种印象下 所有中缀类型构造函数都必须以 a 开头 :.

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

   {-# 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 
   

   但我在使用多参数类型构造函数时遇到问题。有想法吗？

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

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

   难道有某种魔法在发生吗？ Constraint 那种会阻止其作为嵌套对进行操作的类型？

Answer 1

1. 正如评论中所解释的，类型级别的中缀函数不再要求以冒号开头。所以是的，所有这些都是中缀运算符。没有两个中缀运算符会自动相互关联，但单例库在内部使用一些命名约定来关联用于 去功能化 （见下文）给他们的正常同行。

2. 类型族不能部分应用，但数据类型可以，这一事实引发了一大堆问题。这就是为什么单例库使用一种称为 去功能化:对于每个部分应用的类型函数，它定义一个数据类型。然后有一个（非常大且开放的）类型的家庭称为 Apply 它采用所有这些表示部分应用的函数和合适的参数的数据类型并执行实际的应用程序。

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

   TyFun k1 k2 -> *
   

   由于各种原因（顺便说一句，理查德·艾森伯格的博客文章对这一切进行了很好的介绍 “去功能化以求取胜”），而相应的“正常”类型函数的种类将是

   k1 -> k2
   

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

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

   并不是

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

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

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

   第一个参数是一种去功能化的柯里化函数 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]
   

3. 我可能是盲目的，但我不认为这包含在单例中，这与 Constraints。不过，这是一个有用的功能。它是在一个 我目前正在开发的库. 。不过，它还没有完成，而且大部分都没有记录，这就是我还没有发布它的原因。