3

我正在尝试编写两个函数来从 中提取值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列表中类型的第一个元素的签名，并且上下文表明列表实际上包含该类型的一个元素。

extract可以不受约束地写作Typeable吗？

extract'可以不受约束地写作Typeable吗？一个人怎么写Contains？

4

2 回答 2

3

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

此外，我不是 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"
于 2016-02-07T11:47:20.123 回答
3

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。

于 2016-02-08T00:39:24.487 回答