折叠异构编译时列表

Question

我有一个异类型列表(或者至少是我的想法):

data Nul

data Bits b otherBits where 
    BitsLst :: b -> otherBits -> Bits b otherBits 
    NoMoreBits :: Bits b Nul

现在,给定一个输入类型b,我想通过所有Bits类型的板b并总结它们,忽略其他类型的板b' /= b:

class Monoid r => EncodeBit b r | b -> r where 
    encodeBit :: b -> r

class AbstractFoldable aMulti r where 
    manyFold :: r -> aMulti -> r

instance (EncodeBit b r, AbstractFoldable otherBits r) => 
                     AbstractFoldable (Bits b otherBits ) r where 
    manyFold r0 (BitsLst bi other) = manyFold (r0 `mappend` (encodeBit bi)) other
    manyFold b0 NoMoreBits = b0 

instance AbstractFoldable otherBits r =>
                     AbstractFoldable (Bits nb    otherBits ) r where 
    manyFold r0 (BitsLst _ other) = manyFold r0 other
    manyFold b0 NoMoreBits = b0 

但编译器不需要它.并且有充分的理由,因为两个实例声明具有相同的头部.问题:Bits用任意类型折叠的正确方法是什么？

注意:上面的例子是用编译的

{-# LANGUAGE MultiParamTypeClasses, 
             FunctionalDependencies,
             GADTs,
             DataKinds,
             FlexibleInstances,
             FlexibleContexts
#-}

Answer 1

回复您的评论：

\n\n

\n

实际上，如果我可以按类型过滤异构列表，我就可以做到。那可能吗？

\n

\n\n

Typeable如果添加约束，则可以按类型过滤异构列表b。

\n\n

主要思想是我们将使用Data.Typeable\'scast :: (Typeable a, Typeable b) => a -> Maybe b来确定列表中的每个项目是否属于某种类型。这将需要Typeable对列表中的每个项目进行约束。我们将能够检查是否有此约束，而不是构建一个新的列表类型All列表中的类型是否满足某些约束，而不是构建内置此约束的新列表类型。

\n\n

我们的目标是使以下程序输出[True,False]，将异构列表过滤为仅其Bool元素。我将尽力将语言扩展和导入与它们所需的第一个片段一起放置

\n\n

{-# LANGUAGE DataKinds #-}\n{-# LANGUAGE TypeOperators #-}\n\nexample :: HList (Bool \': String \': Bool \': String \': \'[])\nexample = HCons True $ HCons "Jack" $ HCons False $ HCons "Jill" $ HNil\n\nmain = do\n    print (ofType example :: [Bool])\n

\n\n

HList这是 haskell 中异构列表的相当标准的定义，使用DataKinds

\n\n

{-# LANGUAGE GADTs #-}\n{-# LANGUAGE KindSignatures #-}\n\ndata HList (l :: [*]) where\n    HCons :: h -> HList t -> HList (h \': t)\n    HNil :: HList \'[]\n

\n\n

我们想要ofType用这样的签名来编写：“如果All异构列表中的事物是Typeable，则获取特定的那些事物的列表Typeable。

\n\n

import Data.Typeable\n\nofType :: (All Typeable l, Typeable a) => HList l -> [a]\n

\n\n

为此，我们需要All在满足某些约束的类型列表中开发事物的概念。我们将在 a 中存储满足约束的字典，GADT该字典要么捕获头约束字典和All尾部约束，要么证明列表为空。类型列表满足以下约束All如果我们可以捕获类型列表的字典，则类型列表满足其项目

\n\n

{-# LANGUAGE MultiParamTypeClasses #-} \n{-# LANGUAGE ConstraintKinds #-}\n\n-- requires the constraints\xe2\x80\xa0 package.\n-- Constraint is actually in GHC.Prim\n-- it\'s just easier to get to this way\nimport Data.Constraint (Constraint)\n\nclass All (c :: * -> Constraint) (l :: [*]) where\n    allDict :: p1 c -> p2 l -> DList c l\n\ndata DList (ctx :: * -> Constraint) (l :: [*]) where\n    DCons :: (ctx h, All ctx t) => DList ctx (h \': t)\n    DNil  ::                       DList ctx \'[]\n

\n\n

DList实际上是一个字典列表。DCons捕获应用于头项 ( ) 的约束的字典ctx h以及列表其余部分 ( All ctx t) 的所有字典。我们无法直接从构造函数中获取尾部的字典，但我们可以编写一个函数从字典中提取它们All ctx t。

\n\n

{-# LANGUAGE ScopedTypeVariables #-}\n\nimport Data.Proxy\n\ndtail :: forall ctx h t. DList ctx (h \': t) -> DList ctx t\ndtail DCons = allDict (Proxy :: Proxy ctx) (Proxy :: Proxy t)\n

\n\n

类型的空列表可以轻松满足应用于其所有项目的任何约束

\n\n

instance All c \'[] where\n    allDict _ _ = DNil\n

\n\n

如果列表的头部满足约束并且所有尾部也满足，则列表中的所有内容都满足约束。

\n\n

{-# LANGUAGE FlexibleInstances #-}\n{-# LANGUAGE FlexibleContexts #-}\n{-# LANGUAGE UndecidableInstances #-}\n\ninstance (c h, All c t) => All c (h \': t) where\n    allDict _ _ = DCons\n

\n\n

我们现在可以编写ofType，这需要foralls 来确定类型变量的作用域ScopedTypeVariables。

\n\n

import Data.Maybe\n\nofType :: forall a l. (All Typeable l, Typeable a) => HList l -> [a]\nofType l = ofType\' (allDict (Proxy :: Proxy Typeable) l) l\n  where\n    ofType\' :: forall l. (All Typeable l) => DList Typeable l -> HList l -> [a]\n    ofType\' d@DCons (HCons x t) = maybeToList (cast x) ++ ofType\' (dtail d) t\n    ofType\' DNil    HNil        = []\n

\n\n

我们将HList其字典与maybeToList . cast结果压缩在一起并连接起来。我们可以通过以下方式明确这一点RankNTypes。

\n\n

{-# LANGUAGE RankNTypes #-}\n\nimport Data.Monoid (Monoid, (<>), mempty)\n\nzipDHWith :: forall c w l p. (All c l, Monoid w) => (forall a. (c a) => a -> w) -> p c -> HList l -> w\nzipDHWith f p l = zipDHWith\' (allDict p l) l\n  where\n    zipDHWith\' :: forall l. (All c l) => DList c l -> HList l -> w\n    zipDHWith\' d@DCons (HCons x t) = f x <> zipDHWith\' (dtail d) t\n    zipDHWith\' DNil    HNil        = mempty\n\nofType :: (All Typeable l, Typeable a) => HList l -> [a]\nofType = zipDHWith (maybeToList . cast) (Proxy :: Proxy Typeable) \n

\n\n\n\n

\xe2\x80\xa0约束

\n