在 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 superclass 上下文在这里很关键，这是时间问题。 GHC 总是在 before 检查实例约束之前提交一个实例，但在 after 解决 superclass约束。所以我们需要使用 superclass 约束来固定哪些实例为 select.

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

完成此操作后，您实际上可以编写一个接口来避免 "extra" class 参数：

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 是这样的：

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 相同的模式。

在 HList 中查找元素

Find an element in an HList

haskell

hlist