如何提取这个多态递归函数？

我正在使用 GHC 7.8 做一些相当有趣的事情，但遇到了一些问题。我有以下内容：

mkResultF :: Eq k => Query kvs ('KV k v) -> k -> ResultF (Reverse kvs) (Maybe v)
mkResultF Here key = ResultComp (pure . lookup key)
mkResultF q@(There p) key =
  case mkResultF p key of
    ResultFId a -> pure a
    ResultComp c ->
      ResultComp $ \foo ->
       case c foo of
         ResultFId a -> pure a
         ResultComp c ->
           ResultComp $ \foo ->
            case c foo of
              ResultFId a -> pure a

显然这里有一些东西需要抽象，但我不太清楚如何做到这一点。当我尝试以下操作时：

mkResultF :: Eq k => Query kvs ('KV k v) -> k -> ResultF (Reverse kvs) (Maybe v)
mkResultF Here key = ResultComp (pure . lookup key)
mkResultF q@(There p) key = magic (mkResultF p key)

magic :: ResultF (Reverse kvs) (Maybe v) -> ResultF (Reverse kvs ++ '[('KV x y)]) (Maybe v)
magic (ResultFId a) = pure a
magic (ResultComp c) = ResultComp (\foo -> magic (c foo))

这感觉像是一个“明显”的解决方案，但它没有类型检查：

Could not deduce (kvs2 ~ Reverse kvs0)
from the context (Reverse kvs ~ ('KV k v1 : kvs2))
  bound by a pattern with constructor
             ResultComp :: forall a k v (kvs :: [KV * *]).
                           ([(k, v)] -> ResultF kvs a) -> ResultF ('KV k v : kvs) a,
           in an equation for `magic'
  at query-kv.hs:202:8-19
  `kvs2' is a rigid type variable bound by
         a pattern with constructor
           ResultComp :: forall a k v (kvs :: [KV * *]).
                         ([(k, v)] -> ResultF kvs a) -> ResultF ('KV k v : kvs) a,
         in an equation for `magic'
         at query-kv.hs:202:8
Expected type: ResultF (Reverse kvs0) (Maybe v)
  Actual type: ResultF kvs2 (Maybe v)
Relevant bindings include
  c :: [(k, v1)] -> ResultF kvs2 (Maybe v)
    (bound at query-kv.hs:202:19)
In the first argument of `magic', namely `(c foo)'
In the expression: magic (c foo)

我真的很坚持这个。可以在此处找到包含起始代码的完整代码清单：https://gist.github.com/ocharles/669758b762b426a3f930 https://gist.github.com/ocharles/669758b762b426a3f930

为什么你有AllowAmbiguousTypes启用？这几乎从来都不是一个好主意。如果没有扩展名，您会得到更好的错误消息：

Couldn't match type ‘Reverse kvs0’ with ‘Reverse kvs’
NB: ‘Reverse’ is a type function, and may not be injective
The type variable ‘kvs0’ is ambiguous
Expected type: ResultF (Reverse kvs) (Maybe v)
               -> ResultF (Reverse kvs ++ '['KV x y]) (Maybe v)
  Actual type: ResultF (Reverse kvs0) (Maybe v)
               -> ResultF (Reverse kvs0 ++ '['KV x0 y0]) (Maybe v)
In the ambiguity check for:
  forall (kvs :: [KV * *]) v x y.
  ResultF (Reverse kvs) (Maybe v)
  -> ResultF (Reverse kvs ++ '['KV x y]) (Maybe v)
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature for ‘magic’:
  magic :: ResultF (Reverse kvs) (Maybe v)
           -> ResultF (Reverse kvs ++ '[KV x y]) (Maybe v)

问题确实出在类型签名中magic，你在哪里有

magic :: ResultF (Reverse kvs) (Maybe v)
      -> ResultF (Reverse kvs ++ '[('KV x y)]) (Maybe v)

所有变量kvs, x, and y仅作为参数出现Reverse and ++，它们是类型族，不需要是单射的。这样的情况总是很可疑。

最简单的解决方法是添加代理。这是为我编译的代码：

mkResultF :: forall k v kvs. Eq k
           => Query kvs ('KV k v) -> k -> ResultF (Reverse kvs) (Maybe v)
mkResultF Here key = ResultComp (pure . lookup key)
mkResultF (There p) key = magic (Proxy :: Proxy kvs) (mkResultF p key)

magic :: Proxy ('KV x y ': kvs)
      -> ResultF (Reverse kvs) (Maybe v)
      -> ResultF (Reverse ('KV x y ': kvs)) (Maybe v)
magic _ r =
  case r of
    ResultFId a -> pure a
    ResultComp c ->
      ResultComp $ \foo ->
       case c foo of
         ResultFId a -> pure a
         ResultComp c ->
           ResultComp $ \foo ->
            case c foo of
              ResultFId a -> pure a

Edit

我又看了一遍，这是一个使用您定义的版本magic (as magic2）。它仍然不是很优雅，但希望足以作为概念验证：

mkResultF :: forall k v kvs. Eq k
           => Query kvs ('KV k v) -> k -> ResultF (Reverse kvs) (Maybe v)
mkResultF Here      key = ResultComp (pure . lookup key)
mkResultF (There p) key = magic1 (Proxy :: Proxy kvs) (mkResultF p key)

magic1 :: forall x y kvs v. Proxy ('KV x y ': kvs)
       -> ResultF (Reverse kvs) (Maybe v)
       -> ResultF (Reverse ('KV x y ': kvs)) (Maybe v)
magic1 _ = magic2 (Proxy :: Proxy ('KV x y)) (Proxy :: Proxy (Reverse kvs))

magic2 :: Proxy ('KV x y) -> Proxy kvs
       -> ResultF kvs (Maybe v)
       -> ResultF (kvs ++ '[('KV x y)]) (Maybe v)
magic2 _ _ (ResultFId a) = pure a
magic2 p _ (ResultComp (c :: ([(k, v')] -> ResultF kvs' (Maybe v))))
  = ResultComp (\ foo -> magic2 p (Proxy :: Proxy kvs') (c foo))