9

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

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)对的列表中。 )

4

2 回答 2

6

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

首先，您编写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
于 2015-12-21T17:11:13.943 回答
4

我将尝试在这里提出一个“惯用的”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有 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

现在我们必须要求一个额外的约束来表示我们的所有name-s Recare 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后缀都表示普通 -s 的 lambda 项嵌入TyFun（由 TH 生成的另一个简写集合......）。

我有一个原型，尽管由于 GHC 错误，它只适用于更丑陋的 de Bruijn 变量。它还具有Fix类型级别的显式惰性。

于 2015-12-21T21:36:50.427 回答