异构List的映射操作

Question

我有一个简单的异构列表

data HList (ts :: [Type]) where
    HNil :: HList '[]
    (:&:) :: t -> HList ts -> HList (t ': ts)

infixr 5 :&:

我正在尝试定义异构映射：

type family ToDomain (xs :: [Type]) :: [Type] where
    ToDomain '[] = '[];
    ToDomain ((a -> b) ': r) = a ': ToDomain r

type family ToCoDomain (xs :: [Type]) :: [Type] where
    ToCoDomain '[] = '[];
    ToCoDomain ((a -> b) ': r) = b ': ToCoDomain r

mapH :: forall mappings input output.
    (input ~ ToDomain mappings, output ~ ToCoDomain mappings)
    => HList mappings -> HList input -> HList output
mapH HNil HNil = HNil
mapH (f :&: maps) (x :&: ins) = (f x) :&: mapH maps ins

这无法编译（如果这真的有效，我会感到非常惊讶）因为 GHC 无法推断递归的正确性。我不确定如何让 GHC 相信正确性。

Answer 1

你需要证明mappings只有函数在里面。这可以通过额外的 GADT 来实现。

data OnlyFunctions (ts :: [*]) where
   FNil :: OnlyFunctions '[]
   FCons :: OnlyFunctions ts -> OnlyFunctions ((a->b) ': ts)

mapH :: forall mappings input output.
    (input ~ ToDomain mappings, output ~ ToCoDomain mappings)
    => OnlyFunctions mappings -> HList mappings -> HList input -> HList output
mapH FNil HNil HNil = HNil
mapH (FCons h) (f :&: maps) (x :&: ins) = (f x) :&: mapH h maps ins

问题是 ToDomain '[Int,Bool] 是一个有效的类型——即使 ToDomain 在这种情况下没有简化。因此 GHC 不能假定 mappings 类型列表仅由函数组成。

如果需要，您可以通过自定义类型 class 删除附加参数。

class OF (ts :: [*]) where
   onlyFun :: OnlyFunctions ts
instance OF '[] where
   onlyFun = FNil
instance OF ts => OF ((a -> b) ': ts) where
   onlyFun = FCons onlyFun

mapHsimple :: forall mappings input output.
    (input ~ ToDomain mappings, output ~ ToCoDomain mappings, OF mappings)
    => HList mappings -> HList input -> HList output
mapHsimple = mapH onlyFun

Answer 2

如果你想要映射操作，你几乎肯定最好定义

data Rec (f :: k -> *) (ts :: [k]) where
  RNil :: Rec f '[]
  (:&:) :: f t -> Rec f ts -> Rec f (t ': ts)

infixr 5 :&:

现在你可以定义一个通用的

rmap :: (forall a. f a -> g a) -> Rec f ts -> Rec g ts

和

rzipWith :: (forall a. f a -> g a -> h a) -> Rec f ts -> Rec g ts -> Rec h ts

这通常会使事情变得更容易。在这种情况下，您可以使用

data Fun :: * -> * where
  Fun :: (a -> b) -> Fun (a -> b)

data Dom :: * -> * where
  Dom :: a -> Dom (a -> b)

data Cod :: * -> * where
  Cod :: b -> Cod (a -> b)

现在你可以写了

zoop :: Rec Fun fs -> Rec Dom fs -> Rec Cod fs
zoop = rzipWith (\(Fun f) (Dom x) -> Cod (f x))

事实上，其中有些有点矫枉过正；你应该能够摆脱为 Dom 包装类型族的新类型。您甚至可以为 Cod 这样做，但这可能会降低结果的可用性。

异构List的映射操作

mapping operation for heterogenous List

haskell

functor

typeclass