haskell - 异构列表中的单例

我想编写一个分析异类列表的函数。为了争辩，让我们有以下内容

data Rec rs where
  Nil :: Rec '[]
  Cons :: ty -> Rec rs -> Rec ( '(name, ty) ': rs )

class Analyze name ty where
  analyze :: Proxy name -> ty -> Int

最终目标将是编写如下内容

class AnalyzeRec rs where
  analyzeRec :: Rec rs -> [(String, Int)]

instance AnalyzeRec '[] where
  analyzeRec Nil = []

instance (Analyze name ty, AnalyzeRec rs) =>
           AnalyzeRec ( '(name, ty) ': rs )
  where
    analyzeRec (Cons hd tl) =
      let proxy = Proxy :: Proxy name
      in (symbolVal proxy, analyze proxy hd) : analyzeRec tl

突出的位是analyzeRec使用在Rec中每种类型和值实例化的约束知识。这种基于类的机制有效，但是在您必须一遍又一遍(而且我也要这样做)的情况下，它笨拙而冗长。

因此，我想用基于 singletons 的机制代替它。我想写一个类似的函数

-- no type class!
analyzeRec :: All Analyze rs => Rec rs -> [(String, Int)]
analyzeRec rec =
  case rec of
    Nil -> []
    Cons hd tl -> withSing $ \s ->
      (symbolVal s, analyze s hd) : analyzeRec tl

但这显然在至少几个维度上是平坦的。

使用Singletons技术在异构列表上编写此类函数的“正确”方法是什么？有没有更好的方法来解决此问题？解决这类问题我应该期望什么？

(作为参考，这是针对一个名为Serv的实验性Servant克隆。相关文件以 Serv.Internal.Header.Serialization 和 Serv.Internal.Header 作为背景。我想编写一个函数，该函数接收标记的 header 值的异构列表，然后headerEncode将它们编码为实际的(ByteString, ByteString)对。)

最佳答案

我将在此处尝试介绍“惯用的” singletons解决方案(如果甚至存在这种情况)。初步资料:

{-# LANGUAGE
  RankNTypes, DataKinds, PolyKinds, ConstraintKinds, GADTs,
  TypeOperators, MultiParamTypeClasses, TypeFamilies, ScopedTypeVariables #-}

import Data.Singletons.Prelude
import Data.Proxy
import GHC.Exts (Constraint)

-- SingI constraint here for simplicity's sake
class SingI name => Analyze (name :: Symbol) ty where
  analyze :: Proxy name -> ty -> Int

data Rec rs where
  Nil :: Rec '[]
  Cons :: ty -> Rec rs -> Rec ( '(name, ty) ': rs )

recName :: Rec ('(name, t) ': rs) -> Proxy name
recName _ = Proxy

我们需要一个All c rs约束，但是我们给它一个旋转，并将c变成TyFun而不是普通的a -> Constraint构造函数:

type family AllC (c :: TyFun a Constraint -> *) (rs :: [a]) :: Constraint where
  AllC c '[]       = ()
  AllC c (x ': xs) = (c @@ x, AllC c xs)

TyFun使我们可以抽象类型构造函数和类型族，并为我们提供部分应用程序。它为我们提供了几乎一流的类型级别的函数，并且语法有些丑陋。请注意，尽管我们一定会失去构造函数的整体性。 @@是应用TyFun -s的运算符。 TyFun a b -> *表示a是输入，而b是输出，尾随-> *只是编码的工件。有了GHC 8.0，我们将能够做到

type a ~> b = TyFun a b -> *

然后使用a ~> b。

现在我们可以在Rec上实现一个通用的“经典”映射:

cMapRec ::
  forall c rs r.
  AllC c rs => Proxy c -> (forall name t. (c @@ '(name, t)) => Proxy name -> t -> r) -> Rec rs -> [r]
cMapRec p f Nil           = []
cMapRec p f r@(Cons x xs) = f (recName r) x : cMapRec p f xs

请注意，上面的c具有种类TyFun (a, *) Constraint -> *。

然后实现analyzeRec:

analyzeRec ::
  forall c rs. (c ~ UncurrySym1 (TyCon2 Analyze))
  => AllC c rs => Rec rs -> [(String, Int)]
analyzeRec = cMapRec (Proxy :: Proxy c) (\p t -> (fromSing $ singByProxy p, analyze p t))

首先，c ~ UncurrySym1 (TyCon2 Analyze)只是类型级别的let绑定(bind)，它使我可以将c中的Proxy c用作简写。 (如果我真的想使用所有肮脏的技巧，我将添加{-# LANGUAGE PartialTypeSignatures #-}并编写Proxy :: _ c)。

如果Haskell完全支持类型级别的函数，则UncurrySym1 (TyCon2 Analyze)与uncurry Analyze会执行相同的操作。这里的明显优势是，我们可以即时写出analyzeRec的类型，而无需额外的顶级类型族或类，并且还可以更广泛地使用AllC。

另外，让我们从SingI中删除Analyze约束，并尝试实现analyzeRec。

class Analyze (name :: Symbol) ty where
  analyze :: Proxy name -> ty -> Int

现在，我们需要一个额外的约束条件，该约束条件表示name中的所有Rec -s都是SingI。我们可以使用两个cMapRec -s并压缩结果:

analyzeRec ::
  forall analyze names rs.
  (analyze ~ UncurrySym1 (TyCon2 Analyze),
   names   ~ (TyCon1 SingI :.$$$ FstSym0),
   AllC analyze rs,
   AllC names rs)
  => Rec rs -> [(String, Int)]
analyzeRec rc = zip
  (cMapRec (Proxy :: Proxy names)   (\p _ -> fromSing $ singByProxy p) rc)
  (cMapRec (Proxy :: Proxy analyze) (\p t -> analyze p t) rc)

在这里TyCon1 SingI :.$$$ FstSym0可以翻译为SingI . fst。

这仍然大致在可以用TyFun -s表示的抽象级别之内。当然，主要限制是缺少lambda。理想情况下，我们不必使用zip，而是使用AllC (\(name, t) -> (SingI name, Analyze name t))，并使用单个cMapRec。使用singletons，如果我们不能再使用无点类型级编程来扩展它，我们就必须引入一个新的点型类型族。

有趣的是，GHC 8.0足够强大，因此我们可以从头开始实现类型级的lambda，尽管它可能很丑陋。例如，\p -> (SingI (fst p), uncurry Analyze p)可能看起来像这样:

Eval (
  Lam "p" $
    PairL :@@
      (LCon1 SingI :@@ (FstL :@@ Var "p")) :@@
      (UncurryL :@@ LCon2 Analyze :@@ Var "p"))

其中所有L后缀都表示普通TyFun -s的lambda术语嵌入(还有TH生成的另一种速记集合...)。

我有一个prototype，尽管由于GHC错误，它只适用于甚至更难看的de Bruijn变量。它还在类型级别具有Fix和显式惰性。