异构列表中的单身人士

我想编写一个分析异构列表的函数.为了论证,我们有以下几点

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背景一样.我想编写一个函数,它接收标记标题值的异构列表,然后将headerEncode它们放入实际(ByteString, ByteString)对的列表中. )

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

首先,你编写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)]

没有键入检查(它没有很好的kinded).每个元素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