异构列表中的单体

我认为这是一个很好的方法,只是…有时候你需要帮助打字系统。

首先,您编写 All 谓词很重要(如果它在适当的时候减少),我不知道哪一个 全部的 您正在使用。

此外,您正在使用 symbolVal 但没有证据表明它是 KnownSymbol -你必须在某处加上这个证明。对我来说,唯一明显的地方是类型类:

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) 

请注意,这一行

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

我试着在这里介绍一个“惯用语” 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公司 -秒。 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 允许我使用的绑定 c 在里面 Proxy c 作为速记。(如果我真的想使用所有的卑鄙伎俩,我会补充 {-# LANGUAGE PartialTypeSignatures #-} 并写入 Proxy :: _ c ).

UncurrySym1 (TyCon2 Analyze) 做同样的事情 uncurry Analyze 如果Haskell完全支持类型级函数的话,就可以了。这里明显的优点是我们可以写出 分析Rec 不需要额外的顶级类型族或类,也可以使用 AllC 更一般地说。

作为奖励,让我们删除 SingI 约束来自 Analyze ,并尝试实现 分析Rec .

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

现在我们需要一个额外的约束,它表示所有 name -在我们的 记录 是 新加坡 。我们可以用两个 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公司 -秒。当然,主要的限制是缺乏lambdas。理想情况下,我们不必使用 zip ,相反,我们将使用 AllC (\(name, t) -> (SingI name, Analyze name t)) ,并使用单个 cMapRec公司 具有 单光子 ,如果我们不能再使用无点类型级编程,我们必须引入一个新的有点类型族。

有趣的是,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 后缀表示普通的lambda项嵌入 TyFun公司 -s(由TH…生成的另一个速记集合)。

我有一个 prototype ,尽管由于GHC错误,它只适用于更丑陋的de Bruijn变量。它还具有 Fix 以及类型层面的明显懒惰。