haskell - 折叠异构，编译时间，列表

Question

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

data Nul

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

现在，给定一个输入类型 b , 我想遍历 Bits 的所有板 block 类型为 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

回答您的评论:

Actually, I can do if I can filter the heterogeneous list by type. Is that possible?

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

主要思想是我们将使用 Data.Typeable的 cast :: (Typeable a, Typeable b) => a -> Maybe b 确定列表中的每个项目是否属于某种类型。这将需要一个 Typeable列表中每个项目的约束。我们将能够检查 All列表中的类型满足某些约束。

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

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}

example :: HList (Bool ': String ': Bool ': String ': '[])
example = HCons True $ HCons "Jack" $ HCons False $ HCons "Jill" $ HNil

main = do
    print (ofType example :: [Bool])

HList这是在haskell 中使用DataKinds 的异构列表的一个相当标准的定义。

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

data HList (l :: [*]) where
    HCons :: h -> HList t -> HList (h ': t)
    HNil :: HList '[]

我们想写ofType带有类似“如果 All 异构列表中的事物是 Typeable 的签名，则获取特定 Typeable 类型的那些事物的列表。

import Data.Typeable

ofType :: (All Typeable l, Typeable a) => HList l -> [a]

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

{-# LANGUAGE MultiParamTypeClasses #-} 
{-# LANGUAGE ConstraintKinds #-}

-- requires the constraints† package.
-- Constraint is actually in GHC.Prim
-- it's just easier to get to this way
import Data.Constraint (Constraint)

class All (c :: * -> Constraint) (l :: [*]) where
    allDict :: p1 c -> p2 l -> DList c l

data DList (ctx :: * -> Constraint) (l :: [*]) where
    DCons :: (ctx h, All ctx t) => DList ctx (h ': t)
    DNil  ::                       DList ctx '[]

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

{-# LANGUAGE ScopedTypeVariables #-}

import Data.Proxy

dtail :: forall ctx h t. DList ctx (h ': t) -> DList ctx t
dtail DCons = allDict (Proxy :: Proxy ctx) (Proxy :: Proxy t)

一个空的类型列表很容易满足应用于其所有项目的任何约束

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

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

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}

instance (c h, All c t) => All c (h ': t) where
    allDict _ _ = DCons

我们现在可以写ofType , 这需要 forall s 用于使用 ScopedTypeVariables 确定类型变量的范围.

import Data.Maybe

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

我们正在压缩 HList连同它的字典与 maybeToList . cast并连接结果。我们可以使用 RankNTypes 来明确说明。 .

{-# LANGUAGE RankNTypes #-}

import Data.Monoid (Monoid, (<>), mempty)

zipDHWith :: forall c w l p. (All c l, Monoid w) => (forall a. (c a) => a -> w) -> p c -> HList l -> w
zipDHWith f p l = zipDHWith' (allDict p l) l
  where
    zipDHWith' :: forall l. (All c l) => DList c l -> HList l -> w
    zipDHWith' d@DCons (HCons x t) = f x <> zipDHWith' (dtail d) t
    zipDHWith' DNil    HNil        = mempty

ofType :: (All Typeable l, Typeable a) => HList l -> [a]
ofType = zipDHWith (maybeToList . cast) (Proxy :: Proxy Typeable) 

† constraints