数据促销语法 [英] Data Promotion Syntax

问题描述

我最近在 Data.Promotion >单身的。它具有类型族的负载，允许在类型级别进行基本上任意的计算。我有几个使用问题：

1. （$） ， （％$） ， （$$） ，它们是否与：++有关$ ，：。$ ，等等？这些实际上是中缀操作员吗？我在印象之下所有中缀型构造函数都必须以：。




2. 我试图将一个构造函数映射到列表上：

     { - ＃LANGUAGE DataKinds，TypeOperators，PolyKinds＃ - } 
    import Data.Promotion.Prelude 
    
    data Foo ab 
   类型MyList ='[Int，Double，Float] 
    
     - 期望`Foo`多一个参数
    type FooList1 b = Map（（Flip Foo）$ b ）MyList 
    $ b $  - 第二个`b`解析错误
   类型FooList2 b =映射（（$ b）：.Foo）MyList 
     

   但我在使用多参数类型构造函数时遇到了问题。我可以用 Data.Promotion 中的等价函数替换我写的所有类型函数除了这一个：



     type family ListToConstraint（xs :: [Constraint]）::约束
   类型实例ListToConstraint'[] =（）
   类型实例ListToConstraint（x'：xs）=（x，ListToConstraint xs）
     

   使用 Constraint 类型会有什么魔法会阻止它作为嵌套对操作？







解决方案

1. 正如评论中所解释的那样，语法要求类型级别上的中缀函数以冒号开头。所以是的，所有这些都是中缀操作员。没有两个中缀运算符会自动相互关联，但单例库在内部使用了一些命名约定，将用于 defunctionalization 的符号（见下文）与正常对象关联。




2. 类型系列不能部分应用，但数据类型可以。这就是为什么singletons库使用一种名为 defunctionalization 的技术：对于每个部分应用的类型函数，它定义了一个数据类型。然后是一个名为 Apply 的（非常大且开放的）类型家族，它接受所有这些代表部分应用函数和适当参数的数据类型，并执行实际的应用程序。

   
   
   

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

     TyFun k1 k2  - > * 
     

   出于各种原因（顺便说一句，所有这一切都在Richard Eisenberg的博客文章赢取禁用功能），而相应的正常类型函数将是
   

     k1  - > k2 
     

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

     Map ::（TyFun k k1  - > *） - > [k]  - > [k1] 
     

   而不是
   
   

     Map ::（k  - > k1） - > [k]  - > [k1] 
     

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

     Flip ::（TyFun k（TyFun k1 k2  - > *） - > *） - > k1  - > k  - > k2 
     

   第一个参数是类型为 k - >的函数式curry函数。 k1 - > k2 ，然后将它转换为类型为 k1 - >的正常类型函数。 k - >




   （$）::（TyFun k1 k - > *） - > k1 - > k


   这只是应用



   现在我们来看看你的例子：

     type FooList1 b = Map（（Flip Foo）$ b）MyList  - 失败
     

   这里的问题：首先， Foo 是一个数据类型，而不是作为 Flip 期望的去功能化符号。其次， Flip 是一个类型族，期望三个参数，但只提供一个参数。我们可以通过应用 TyCon2 来解决第一个问题，它使用一个普通的数据类型并将它变成一个去功能化的符号：

<$ （k-> k1-> k2） - > TyFun k（TyFun k1 k2 - > *） - > *


   对于第二个问题，我们需要的部分应用程序之一翻转

     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> ：类！ 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 ）。总而言之：
   $ b $ pre $ type FooList2 b = Map（（FlipSym2（$$）b）：。$$$ TyCon2 Foo） MyList


   再说一遍，这是可行的：
   
   

     GHCI> ：类！ FooList2 Char 
    FooList2 Char :: [*] 
    ='[Foo Int Char，Foo Double Char，Foo Float Char] 
     




3. 我可能是盲人，但我不认为这包含在单身人士中，这并不是很关心约束秒。不过，这是一个有用的功能。它位于我目前正在使用的图书馆中。尽管如此，它还没有完成，大部分都没有记录，这就是为什么我还没有发布它。




I recently discovered the Data.Promotion half of singletons. It has loads of type families which allow essentially arbitrary computation at the type level. I have a couple of questions about usage:

1. What is the difference between ($), (%$), ($$), and are they related to :++$, :.$, etc? Are these actually infix operators? I was under the impression all infix type constructors had to begin with a :.

2. I'm trying to map a constructor over a list:

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

   but I'm having trouble using a multi-parameter type constructor. Ideas?

3. I was able to replace all of the type functions I had written with equivalent functions from Data.Promotion except this one:

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

   Is there some kind of magic going on with the Constraint kind that would prevent its manipulation as nested pairs?

解决方案

1. As has been explained in the comments, there's no longer a syntactic requirement for infix functions on the type level to start with a colon. So yes, all these are infix operators. No two infix operators are automatically related to each other, but the singletons library uses some naming conventions internally, to relate symbols used for defunctionalization (see below) to their normal counterparts.

2. There's a whole bunch of problems arising from the fact that type families cannot be partially applied, but datatypes can. That's why the singletons library uses a technique called defunctionalization: for each partially applied type function, it defines a datatype. There's then a (very large and open) type family called Apply that takes all these datatypes that represent partially applied functions and suitable arguments and performs the actual application.

   The kind of such defunctionalized representations of type functions is

   TyFun k1 k2 -> *
   

   for various reasons (btw, a good introduction to all this is in Richard Eisenberg's blog post "Defunctionalization for the win"), whereas the kind of the corresponding "normal" type function would be

   k1 -> k2
   

   Now all higher-order type functions in singletons expect defunctionalized arguments. For example, the kind of Map is

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

   and not

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

   Now let's look at the functions you're working with:

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

   The first argument is a defunctionalized curried function of kind k -> k1 -> k2, and it turns this into a normal type function of kind k1 -> k -> k2.

   Also:

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

   This is just a synonym for the Apply I mentioned above.

   Now let's look at your example:

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

   There are two problems here: First, Foo is a datatype and not a defunctionalized symbol as Flip expects. Second, Flip is a type family and expects three arguments, but only one is provided. We can fix the first problem by applying TyCon2, which takes a normal datatype and turns it into a defunctionalized symbol:

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

   For the second problem, we need one of the partial applications of Flip that singletons already defines for us:

   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
   

   If you look closely, then FlipSymN is the representation required if Flip is partially applied to N arguments, and Flip corresponds to the imaginary FlipSym3. In the example, Flip is applied to one argument, so the corrected example becomes

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

   And this works:

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

   The second example is similar:

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

   Here, we have the following problems: again, Foo must be turned into a defunctionalized symbol using TyCon2; operator sections such as $ b are not available on the type level, hence the parse error. We'll have to use Flip again, but this time FlipSym2, because we apply it to the operator $ and b. Oh, but then $ is partially applied, so we need a symbol corresponding to $ with 0 arguments. This is available as $$ in singletons (for symbolic operators, the defunctionalized symbols have appended $s). And finally, :. is also partially applied: it expects three operators, but has been given only two. So we go from :. to :.$$$ (three dollars because one dollar corresponds to 0, and three dollars correspond to 2). All in all:

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

   And again, this works:

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

3. I may be blind, but I don't think this is contained in singletons, which is not all that much concerned with Constraints. It's a useful function, though. It's in a library I'm currently working on. It's still unfinished and mostly undocumented, though, that's why I haven't released it yet.

这篇关于数据促销语法的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！