我怎样才能提取这种多态递归函数？
我用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
为什么你启用了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和y仅作为参数Reverse和++ ，它们是类型族，不必是内射的。 比如情况总是令人怀疑。
最简单的解决方法是添加代理。 这里是为我编译的代码：
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
编辑
我又看了一遍，这是一个使用magic定义的版本（如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))
上一篇: How can I extract this polymorphic recursion function?
下一篇: Haskell: use of unsafePerformIO for global constant bindings