haskell - HListElim 可以与其他函数组合吗？

Question

给定

{-# LANGUAGE TypeFamilies, KindSignatures #-}
{-# LANGUAGE GADTs, DataKinds, TypeOperators #-}

import Data.HList
import Data.Singletons
import Data.Singletons.Prelude.List

type family HListElim (ts :: [*]) (a :: *) :: * where
    HListElim '[] a = a
    HListElim (t ': ts) a = t -> HListElim ts a

hListUncurry :: HListElim ts a -> HList ts -> a
hListUncurry f HNil = f
hListUncurry f (HCons x xs) = hListUncurry (f x) xs

hListCurryExpl :: Sing ts -> (HList ts -> a) -> HListElim ts a
hListCurryExpl SNil f = f HNil
hListCurryExpl (SCons _ r) f = \x -> hListCurryExpl r (f . HCons x)

hListCurry :: SingI ts => (HList ts -> a) -> HListElim ts a
hListCurry = hListCurryExpl sing

(改编自https://gist.github.com/timjb/516f04808f0c4aa90c26和reroute)

我希望能够编写如下所示的函数

hListCompose :: (a -> b) -> HListElim as a -> HListElim as b

我的第一次尝试是

hListCompose f g = hListCurry (fmap f (hListUncurry g))

但是 GHC 告诉我

Could not deduce (HListElim ts0 b ~ HListElim ts b)
from the context (HasRep ts)
  bound by the inferred type for ‘hListCompose’:
             HasRep ts => (a -> b) -> HListElim ts a -> HListElim ts b
  at src/Webcrank/Wai/T.hs:64:1-55
NB: ‘HListElim’ is a type function, and may not be injective
The type variable ‘ts0’ is ambiguous
Expected type: (a -> b) -> HListElim ts a -> HListElim ts b
  Actual type: (a -> b) -> HListElim ts0 a -> HListElim ts0 b
When checking that ‘hListCompose’
  has the inferred type ‘forall (ts :: [*]) a b.
                         SingI ts =>
                         (a -> b) -> HListElim ts a -> HListElim ts b’
Probable cause: the inferred type is ambiguous

这可能吗？

Answer 1

GHC 在这种情况下是正确的:基本问题是，因为类型族不需要单射，所以 HListElim as a 不指定 as 是什么。 (要了解原因，请考虑 HListElim '[] (a -> b) ~ HListElim '[a] b)。

如果您愿意向 hListCompose 添加额外的 Singleton 参数以明确给出 HList，则可以解决此问题:

{-# LANGUAGE ScopedTypeVariables #-}
hListCompose :: forall a b as. Sing as -> (a -> b) -> HListElim as a -> HListElim as b
hListCompose s f = go s
  where
    go :: forall ts. Sing ts -> HListElim ts a -> HListElim ts b
    go SNil = f
    go (SCons _ ts) = \g x -> go ts (g x)