异构列表中的单身人士

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

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

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

(作为参考,这是一个名为Serv的实验性Servant克隆.相关文件是Serv.Internal.Header.Serialization和Serv.Internal.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)]

没有键入检查(它没有很好的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

Answer 2

我将尝试在这里提出一个“惯用”的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让我们对类型构造函数和类型族进行抽象，并为我们提供部分应用程序。它为我们提供了几乎一流的类型级函数，但语法有些丑陋。但请注意，我们必然会失去构造函数的单射性。@@是应用 -s 的运算符TyFun。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有 kind 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绑定，让我可以使用cinProxy c作为简写。（如果我真的想使用所有肮脏的技巧，我会添加{-# LANGUAGE PartialTypeSignatures #-}并编写Proxy :: _ c）。

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

作为奖励，让我们删除SingI的约束Analyze，并尝试实现analyzeRec。

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

现在我们必须需要一个额外的约束来表示nameour 中的所有 -sRec都是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.

这仍然大致在可以用 -s 轻松表达的抽象级别内TyFun。当然，主要的限制是缺少 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后缀表示普通 -s 的 lambda 项嵌入TyFun（另一个由 TH 生成的简写集合...）。

我有一个原型，尽管由于 GHC bug，它只能与更丑陋的 de Bruijn 变量一起使用。它还Fix在类型级别上具有明显的惰性。