数据提升语法

Question

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

1. 是什么区别($),(%$),($$),和他们在有关:++$,:.$等等？这些实际上是中缀运营商吗？我的印象是所有中缀类型的构造函数都必须以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. 由于类型族不能部分应用,但数据类型可以,因此会产生大量问题.这就是为什么单例库使用一种称为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
   

   第一个参数是类型的defunctionalized curried函数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,它采用普通的数据类型并将其转换为一个defunctionalized符号:

   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必须使用变成一个defunctionalized符号TyCon2; 诸如$ b类型级别上不可用的运算符部分,因此解析错误.我们将不得不Flip再次使用,但这一次FlipSym2,因为我们将它应用于运营商$和b.哦,但随后$部分应用,所以我们需要一个对应$0参数的符号.这可以像$$单体一样使用(对于符号运算符,defunctionalized符号附加$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. 我可能是盲人,但我认为这不包含在单身人士身上,而单身人士并不十分关心单身人士Constraint.不过,这是一个有用的功能.它在我正在研究的图书馆里.它仍然未完成,大部分都没有记录,但这就是为什么我尚未发布它.