在 HList 中查找元素

Question

我正在尝试编写两个函数来从 HList 中提取值，但我似乎无法让 GHC 满意。

第一个函数将具有签名extract :: HList a -> [b]，它从列表中提取b 类型的所有元素。我只是通过要求a 中的类型拥有Typeable 实例才成功编写它。

class OfType a b where
    oftype :: a -> [Maybe b]

instance OfType (HList '[]) b where
    oftype = const []

instance (Typeable t, Typeable b, OfType (HList ts) b) => OfType (HList (t ': ts)) b where
    oftype (x :- xs) = (cast x :: Maybe b) : oftype xs

extract :: OfType a b => a -> [b]
extract = catMaybes . oftype

这是次优的，因为实际上并不需要 Typeable 约束来编写任何提取实例。

我尝试在约束中使用类型等式和不等式，但这只会给我重叠的实例。

我尝试编写的第二个函数将具有签名extract' :: Contains h n => HList h -> n，它提取列表中n 类型的第一个元素，并且上下文表明该列表实际上包含该类型的一个元素。

是否可以在没有Typeable 约束的情况下编写extract？

是否可以在没有Typeable 约束的情况下编写extract'？ 怎么写Contains？

Answer 1

由于您想在编译时检查类型相等性，我相信重叠实例是不可避免的（而且我不喜欢这些......）。

另外，我不能 100% 确定我得到了正确的重叠编译指示。

{-# LANGUAGE DataKinds, TypeOperators, ScopedTypeVariables,
    MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}
{-# OPTIONS -Wall #-}
module HListFilter where

import Data.HList.HList

class OfType a b where
    oftype :: a -> [b]

instance OfType (HList '[]) b where
    oftype = const []

instance {-# OVERLAPS #-} (OfType (HList ts) t) => OfType (HList (t ': ts)) t where
    oftype (HCons x xs) = x : oftype xs

instance {-# OVERLAPPABLE #-} (OfType (HList ts) b) => OfType (HList (t ': ts)) b where
    oftype (HCons _ xs) = oftype xs

test :: HList '[Int, Char, [Char], Char, Bool]
test = HCons (1::Int) (HCons 'a' (HCons "foo" (HCons 'b' (HCons True HNil))))

test_result :: [Char]
test_result = oftype test  -- "ab"

Answer 2

András Kovács 提到了类型族方法。这是一种方法：

type family Equal (x :: *) (y :: *) where
  Equal x x = 'True
  Equal x y = 'False

type family Check (b :: *) (as :: [*]) :: [Bool] where
  Check b '[] = '[]
  Check b (a ': as) = (b `Equal` a) ': Check b as

class ps ~ Check b as =>
    OfType (ps :: [Bool]) (as :: [*]) b where
  extract :: HList as -> [b]

ps ~ Check b as 超类上下文在这里很关键，只是时间问题。 GHC 总是在检查实例约束之前 提交一个实例，但它甚至在解决超类约束之后 之前都不会尝试找到一个实例。所以我们需要使用超类约束来固定选择哪些实例。

instance OfType '[] '[] b where
  extract HNil = []

instance (OfType ps as b, a ~ b) =>
           OfType ('True ': ps) (a ': as) b where
  extract (HCons x xs) = x : extract xs

instance (OfType ps as b, Equal b a ~ 'False) =>
    OfType ('False ': ps) (a ': as) b where
  extract (HCons _ xs) = extract xs

完成此操作后，您实际上可以编写一个避免“额外”类参数的接口：

class OfType' (as :: [*]) (b :: *) where
  extract' :: HList as -> [b]

instance OfType ps as b => OfType' as b where
  extract' = extract

---

写Contains 和extract' 很容易。然而，编写好的Contains 的实例 需要与OfType 完全相同的箍跳。你想要的课程是这样的：

class Contains xs y where
  contains :: y `Elem` xs

-- Elem is part of the dependently typed folklore.
data Elem y xs where
  Here :: Elem y (y ': xs)
  There :: Elem y xs -> Elem y (x ': xs)

但是编写实例将再次迫使您进入重叠或封闭的类型系列。我知道我已经在 SO 附近的某个地方编写了这段代码，但是您应该能够很容易地计算出重叠版本；类型家族版本通常会遵循与OfType 相同的模式。