问题描述
我用GHC 7.8做了相当有趣的事情,但遇到了一些问题。我有以下内容:为什么你要启用 AllowAmbiguousTypes ?这几乎从来都不是一个好主意。没有扩展名,你会得到一个更好的错误信息:
无法将类型'Reverse kvs0'与'Reverse kvs'
NB:'Reverse'是一个类型函数,可能不是内注
类型变量'kvs0'不明确
期望类型:ResultF(反向kvs)(也许v)
- > (可能是v)
实际类型:ResultF(反向kvs0)(也许是v)
- > ResultF(反向kvs ++'['KV x y])在
forall(kvs :: [KV * *])v x y的模糊检查中。
ResultF(反向kvs)(也许v)
- >为了推迟歧义检查以使用站点,启用AllowAmbiguousTypes
在'magic'的类型签名中:
magic :: ResultF(Reverse kvs)(也许是v)
- > ResultF(Reverse kvs ++'[KV xy])(Maybe v)
问题的确在 magic 的类型签名,您有
magic :: ResultF (反向kvs)(也许是v)
- > ResultF(Reverse kvs ++'[('KV xy)])(Maybe v)
所有变量 kvs , x 和 y 仅作为参数出现至反转和 ++ ,这是类型族,不需要是内射的。如情况总是可疑。
最简单的解决方法是添加代理。以下是为我编译的代码:
mkResultF :: forall k v kvs。公式k
=>查询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)
$ b $ magic:代理('KV xy':kvs)
- > ResultF(Reverse kvs)(Maybe v)
- > ResultF(Reverse('KV x y':kvs))(Maybe v)
magic _ r =
case r of
ResultFId a - >纯a
ResultComp c - >
ResultComp $ \foo - >
case c foo
ResultFId a - >纯a
ResultComp c - >
ResultComp $ \foo - >
case c foo
ResultFId a - >纯a
编辑
我已经看过这个了,下面是一个使用 magic 定义的版本(如 magic2 )。它仍然不是很优雅,但它足以作为一个概念证明:
mkResultF :: forall k v kvs。公式k
=>查询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 xy kvs v。Proxy('KV xy':kvs)
- > ResultF(Reverse kvs)(Maybe v)
- > ResultF(Reverse('KV xy':kvs))(Maybe v)
magic1 _ = magic2(Proxy :: Proxy('KV xy))(Proxy :: Proxy(Reverse kvs))
magic2 :: Proxy('KV xy) - >代理kvs
- > ResultF kvs(也许v)
- > ResultF(cvs([KV xy)])(也许v)
magic2 _ _(ResultFId a)=纯a
magic2 p _ ($ f $)=> ResultF kvs'(Maybe v))))
= ResultComp(\ foo - > magic2 p(Proxy :: Proxy kvs')(c foo))
I'm doing so fairly fun stuff with GHC 7.8, but have ran in to a bit of a problem. I have the following:
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 aClearly there is something to abstract here, but I can't quite work out how to do it. When I try the following:
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))This feels like an "obvious" solution, but it doesn't type check:
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)I'm really stuck on this. A full code listing with the starting code can be found here: https://gist.github.com/ocharles/669758b762b426a3f930
解决方案Why do you have AllowAmbiguousTypes enabled? That's almost never a good idea. Without the extension, you get a much better error message:
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)The problem is indeed in the type signature for magic, where you have
magic :: ResultF (Reverse kvs) (Maybe v) -> ResultF (Reverse kvs ++ '[('KV x y)]) (Maybe v)All the variables kvs, x, and y occur only as arguments to Reverse and ++, which are type families and need not be injective. Such as situation is always suspicious.
The easiest fix is to add a proxy. Here's code that compiles for me:
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 aEdit
I've looked at this again, and here's a version that uses your definition of magic (as magic2). It's still not very elegant, but it hopefully suffices as a proof-of-concept:
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))
这篇关于我怎样才能提取这种多态递归函数?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!