haskell - 异构列表中的单例

Question

我想编写一个分析异构列表的函数。为了便于论证，我们有以下内容

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

但这显然至少在几个方面是平淡的。

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

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

Answer 1

我认为这是一个合理的方法，只是......有时你需要帮助类型系统。

首先，您编写 All 谓词的方式非常重要(如果它在适当的时间减少)，而且我不知道您正在使用哪个 All。

此外，您在名称上使用了 symbolVal，但没有证据表明它是 KnownSymbol - 您必须在某处添加此证明。对我来说，唯一明显的地方是类型类:

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

这是All谓词:

type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where 
  All c '[] = () 
  All c (x ': xs) = (c x, All c xs) 

请注意这一行

analyzeRec :: All Analyze rs => Rec rs -> [(String, Int)]

不进行类型检查(这不是很好)。 rs 的每个元素都是一个元组。我们可以直接编写 All'::(k0 -> k1 -> Constraint) -> [(k0,k1)] -> Constraint ，方式与 All' 相同>。但编写一个类型类 Uncurry 更有趣:

type family Fst (x :: (k0, k1)) :: k0 where 
  Fst '(x,y) = x 

type family Snd (x :: (k0, k1)) :: k1 where 
  Snd '(x,y) = y 

class (c (Fst x) (Snd x)) => Uncurry (c :: k0 -> k1 -> Constraint) (x :: (k0, k1)) where 
instance (c x y) => Uncurry c '(x, y)

如果这个 Uncurry 看起来极其复杂，那也是因为 Uncurry c '(x,y) 简化为 c x y 非常重要> 在正确的时间，因此它的编写方式会强制(或者更确切地说允许)类型检查器在看到它时减少此约束。现在的功能是

analyzeRec :: All (Uncurry Analyze) rs => Rec rs -> [(String, Int)]
analyzeRec r = 
  case r of
    Nil -> []
    (Cons hd tl) -> let s = recName r in (symbolVal s, analyze s hd) : analyzeRec tl

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

这不使用 singletons 中的任何内容，也不需要它。

<小时/>

完整的工作代码

{-# LANGUAGE PolyKinds, ConstraintKinds, UndecidableInstances, TypeOperators #-}
{-# LANGUAGE DataKinds, GADTs, MultiParamTypeClasses, TypeFamilies, FlexibleInstances, FlexibleContexts #-} 

import Data.Proxy 
import GHC.TypeLits 
import GHC.Prim (Constraint)

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

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

type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where 
  All c '[] = () 
  All c (x ': xs) = (c x, All c xs) 

type family Fst (x :: (k0, k1)) :: k0 where 
  Fst '(x,y) = x 

type family Snd (x :: (k0, k1)) :: k1 where 
  Snd '(x,y) = y 

class (c (Fst x) (Snd x)) => Uncurry (c :: k0 -> k1 -> Constraint) (x :: (k0, k1)) where 
instance (c x y) => Uncurry c '(x, y)

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

analyzeRec :: All (Uncurry Analyze) rs => Rec rs -> [(String, Int)]
analyzeRec r = 
  case r of
    Nil -> []
    (Cons hd tl) -> let s = recName r in (symbolVal s, analyze s hd) : analyzeRec tl