3

给定

{-# 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并重新路由）

我希望能够编写如下函数

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

这甚至可能吗？

4

1 回答 1

2

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

如果您愿意添加一个额外的Singleton 参数来明确hListCompose给出：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)
于 2015-03-13T01:42:13.673 回答