7

我有一个异构类型的列表（或者至少这是我的想法）：

data Nul

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

现在，给定一个输入 type b，我想遍历所有Bits带有 type的板块b并总结它们，忽略其他带有 type 的板块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
#-}
4

1 回答 1

2

回答您的评论：

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

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

主要思想是我们将使用Data.Typeable'scast :: (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。我们不能直接从构造函数中获取 tail 的字典，但是我们可以编写一个函数从字典中提取它们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，这需要foralls 来使用 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)

†<a href="http://hackage.haskell.org/package/constraints" rel="nofollow">约束

于 2015-06-18T17:27:09.337 回答