什么时候-XAllowAmbiguousTypes适合？ [英] When is -XAllowAmbiguousTypes appropriate?
问题描述
我最近发布了关于问题 github.com/emilaxelsson/syntacticrel =nofollow noreferrer>语法-2.0 有关 share 的定义。 GHC 7.6 ：
{ - ＃LANGUAGE GADTs，TypeOperators，FlexibleContexts ＃ - }
import Data.Syntactic
import Data.Syntactic.Sugar.BindingT
data让a where
让:: Let（a： （a - > b）： - >完整b）
share ::（让：，
sup〜Domain b，sup〜Domain a，
句法a，句法b，
句法（a - > b），
SyntacticN（a - >（a - > b） - > b）
fi ）
=> a - > （a - > b） - > b
share = sugarSym让
但是，GHC 7.8希望 - XAllowAmbiguousTypes 用该签名进行编译。或者，我可以用
替换 fi （ASTF sup（Internal a） - > AST sup（（内部a）： - >完整（内部b）） - > ASTF sup（内部b））
这是fundep在 SyntacticN 中隐含的类型。这允许我避免扩展。当然这是
我的问题是：
- 是否可以接受
-XAllowAmbiguousTypes？ - 一般来说，什么时候应该使用这个扩展？一个答案在这里表明这几乎是从来不是一个好主意。
-
虽然我读过文档，我仍然无法确定约束是否含糊不清。具体来说，从Data.Syntactic.Sugar考虑这个函数：
sugarSym ::（sub：<：AST sup，ApplySym sig fi sup，SyntacticN f fi）
=>子信号 - > f
sugarSym = sugarN。 appSym
在我看来，
fi（并且可能sup）在这里应该是不明确的，但是它没有扩展就编译。为什么sugarSym不明确，而share是？由于share是sugarSym的应用程序，所以share约束都来自sugarSym。
我没有看到 sugarSym 的签名使用了那些确切类型名称的任何已发布语法版本，所以我将使用开发分支在提交8cfd02 ^ ，最后一个版本仍然使用这些名称。
那么，为什么GHC会在您的类型签名中抱怨 fi ，但不是 sugarSym ？您链接到的文档解释了，如果类型不出现在约束条件的右侧，则该类型是不明确的，除非约束使用函数依赖关系来从其他非歧义类型推断否则不明确的类型。因此，让我们比较这两个函数的上下文并查找函数依赖关系。
class ApplySym sig f sym | sig sym - > f，f - > sig sym
class SyntacticN f internal | f - >内部
sugarSym ::（sub：< ;: AST sup
，ApplySym sig $ sup
，SyntacticN f $
）
=>子信号 - > f
share ::（Let：<：sup
，sup〜Domain b
，sup〜Domain a
，Syntactic a
，Syntactic （a - > b）
，SyntacticN（a - >（a - > b） - > b）fi
）
=> a - > （a - > b） - > b
因此，对于 sugarSym 不明确的类型是 sub ， sig 和 f ，并且来自那些我们应该能够遵循函数依赖来消除在上下文中使用的所有其他类型，即 sup 和 fi 。事实上， f - > 中的内部函数依赖项使用我们的 f 来消除我们的 fi ，然后 f - > sig sym 函数依赖在 ApplySym 中使用了我们新消歧的 fi 来消除 sup （和 sig ，这已经是非歧义的）。这就解释了为什么 sugarSym 不需要 AllowAmbiguousTypes 扩展名。
现在让我们看看 sugar 。我注意到的第一件事是编译器不是抱怨模糊的类型，而是关于重叠的实例：
SyntacticN的重叠实例b fi
由于'share'的歧义检查而产生
匹配givens（或其超类）：
（SyntacticN（a - > > b） - > b）fi1）
匹配实例：
实例[overlap ok]（语法f，域f〜sym，
fi〜AST sym（Full（Internal f） ））=>
SyntacticN f $
- 在'Data.Syntactic.Sugar'中定义
实例[overlap ok]（Syntactic a，Domain a〜sym，
ia〜Internal a，SyntacticN f fi）=>
SyntacticN（a - > f）（AST sym（Full ia） - > fi）
- 在'Data.Syntactic.Sugar'中定义
（选择取决于实例化'b，fi'）
要推迟使用网站的歧义检查，启用AllowAmbiguousTypes
因此，如果我正在阅读此权利，并不是说GHC认为您的类型不明确，而是在检查您的类型是否含糊不清时，GHC会遇到不同的单独问题。然后它会告诉你，如果你告诉GHC不要执行模糊检查，它不会遇到这个单独的问题。这解释了为什么启用AllowAmbiguousTypes允许您的代码进行编译。
但是，重叠实例的问题依然存在。 GHC列出的两个实例（ SyntacticN ffi 和 SyntacticN（a - > f）... ）相互重叠。奇怪的是，它们中的第一个似乎应该与任何其他可疑的实例重叠。而且 [overlap ok] 是什么意思？
我怀疑Syntactic是用OverlappingInstances编译的。并查看代码，的确如此。
实验一下，似乎GHC对于重叠实例来说是可以的，当它清楚地表明一个比另一个更一般时：
{ - ＃LANGUAGE FlexibleInstances，OverlappingInstances＃ - }
class Foo a where
whichOne :: a - >字符串
实例Foo a其中
whichOne _ =a
实例Foo [a]其中
whichOne _ =[a]
- |
- >>> main
- [a]
main :: IO（）
main = putStrLn $ whichOne（undefined :: [Int]）
但是GHC对重叠的实例并不合适，但两者显然都不如其他实体：
{ - ＃LANGUAGE FlexibleInstances，OverlappingInstances＃ - }
class Foo a where
whichOne :: a - >字符串
实例Foo（f Int）其中 - 这是更改
whichOne _ =f Int
实例Foo [a]其中
whichOne _ =[a]
- |
- >>> main
- 错误：为Foo [Int]重叠实例
main :: IO（）
main = putStrLn $ whichOne（undefined :: [Int]）
您的类型签名使用 SyntacticN（a - >（a - > b） - > b） fi ，既不 SyntacticN f fi 也不 SyntacticN（a - > f）（AST sym（Full ia） - > fi）比另一个更好。如果我将你的类型签名的那部分改为 SyntacticN a fi 或 SyntacticN（a - >（a - > b） - > b ）（AST sym（Full ia） - > fi），GHC不再抱怨重叠。
I've recently posted a question about syntactic-2.0 regarding the definition of share. I've had this working in GHC 7.6:
{-# LANGUAGE GADTs, TypeOperators, FlexibleContexts #-}
import Data.Syntactic
import Data.Syntactic.Sugar.BindingT
data Let a where
Let :: Let (a :-> (a -> b) :-> Full b)
share :: (Let :<: sup,
sup ~ Domain b, sup ~ Domain a,
Syntactic a, Syntactic b,
Syntactic (a -> b),
SyntacticN (a -> (a -> b) -> b)
fi)
=> a -> (a -> b) -> b
share = sugarSym Let
However, GHC 7.8 wants -XAllowAmbiguousTypes to compile with that signature. Alternatively, I can replace the fi with
(ASTF sup (Internal a) -> AST sup ((Internal a) :-> Full (Internal b)) -> ASTF sup (Internal b))
which is the type implied by the fundep on SyntacticN. This allows me to avoid the extension. Of course this is
- a very long type to add to an already-large signature
- tiresome to manually derive
- unnecessary due to the fundep
My questions are:
- Is this an acceptable use of
-XAllowAmbiguousTypes? - In general, when should this extension be used? An answer here suggests "it is almost never a good idea".
Though I've read the docs, I'm still having trouble deciding if a constraint is ambiguous or not. Specifically, consider this function from Data.Syntactic.Sugar:
sugarSym :: (sub :<: AST sup, ApplySym sig fi sup, SyntacticN f fi) => sub sig -> f sugarSym = sugarN . appSymIt appears to me that
fi(and possiblysup) should be ambiguous here, but it compiles without the extension. Why issugarSymunambiguous whileshareis? Sinceshareis an application ofsugarSym, theshareconstraints all come straight fromsugarSym.
I don't see any published version of syntactic whose signature for sugarSym uses those exact type names, so I'll be using the development branch at commit 8cfd02^, the last version which still used those names.
So, why does GHC complain about the fi in your type signature but not the one for sugarSym? The documentation you have linked to explains that a type is ambiguous if it doesn't appear to the right of the constraint, unless the constraint is using functional dependencies to infer the otherwise-ambiguous type from other non-ambiguous types. So let's compare the contexts of the two functions and look for functional dependencies.
class ApplySym sig f sym | sig sym -> f, f -> sig sym
class SyntacticN f internal | f -> internal
sugarSym :: ( sub :<: AST sup
, ApplySym sig fi sup
, SyntacticN f fi
)
=> sub sig -> f
share :: ( Let :<: sup
, sup ~ Domain b
, sup ~ Domain a
, Syntactic a
, Syntactic b
, Syntactic (a -> b)
, SyntacticN (a -> (a -> b) -> b) fi
)
=> a -> (a -> b) -> b
So for sugarSym, the non-ambiguous types are sub, sig and f, and from those we should be able to follow functional dependencies in order to disambiguate all the other types used in the context, namely sup and fi. And indeed, the f -> internal functional dependency in SyntacticN uses our f to disambiguate our fi, and thereafter the f -> sig sym functional dependency in ApplySym uses our newly-disambiguated fi to disambiguate sup (and sig, which was already non-ambiguous). So that explains why sugarSym doesn't require the AllowAmbiguousTypes extension.
Let's now look at sugar. The first thing I notice is that the compiler is not complaining about an ambiguous type, but rather, about overlapping instances:
Overlapping instances for SyntacticN b fi
arising from the ambiguity check for ‘share’
Matching givens (or their superclasses):
(SyntacticN (a -> (a -> b) -> b) fi1)
Matching instances:
instance [overlap ok] (Syntactic f, Domain f ~ sym,
fi ~ AST sym (Full (Internal f))) =>
SyntacticN f fi
-- Defined in ‘Data.Syntactic.Sugar’
instance [overlap ok] (Syntactic a, Domain a ~ sym,
ia ~ Internal a, SyntacticN f fi) =>
SyntacticN (a -> f) (AST sym (Full ia) -> fi)
-- Defined in ‘Data.Syntactic.Sugar’
(The choice depends on the instantiation of ‘b, fi’)
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
So if I'm reading this right, it's not that GHC thinks that your types are ambiguous, but rather, that while checking whether your types are ambiguous, GHC encountered a different, separate problem. It's then telling you that if you told GHC not to perform the ambiguity check, it would not have encountered that separate problem. This explains why enabling AllowAmbiguousTypes allows your code to compile.
However, the problem with the overlapping instances remain. The two instances listed by GHC (SyntacticN f fi and SyntacticN (a -> f) ...) do overlap with each other. Strangely enough, it seems like the first of these should overlap with any other instance, which is suspicious. And what does [overlap ok] mean?
I suspect that Syntactic is compiled with OverlappingInstances. And looking at the code, indeed it does.
Experimenting a bit, it seems that GHC is okay with overlapping instances when it is clear that one is strictly more general than the other:
{-# LANGUAGE FlexibleInstances, OverlappingInstances #-}
class Foo a where
whichOne :: a -> String
instance Foo a where
whichOne _ = "a"
instance Foo [a] where
whichOne _ = "[a]"
-- |
-- >>> main
-- [a]
main :: IO ()
main = putStrLn $ whichOne (undefined :: [Int])
But GHC is not okay with overlapping instances when neither is clearly a better fit than the other:
{-# LANGUAGE FlexibleInstances, OverlappingInstances #-}
class Foo a where
whichOne :: a -> String
instance Foo (f Int) where -- this is the line which changed
whichOne _ = "f Int"
instance Foo [a] where
whichOne _ = "[a]"
-- |
-- >>> main
-- Error: Overlapping instances for Foo [Int]
main :: IO ()
main = putStrLn $ whichOne (undefined :: [Int])
Your type signature uses SyntacticN (a -> (a -> b) -> b) fi, and neither SyntacticN f fi nor SyntacticN (a -> f) (AST sym (Full ia) -> fi) is a better fit than the other. If I change that part of your type signature to SyntacticN a fi or SyntacticN (a -> (a -> b) -> b) (AST sym (Full ia) -> fi), GHC no longer complains about the overlap.
If I were you, I would look at the definition of those two possible instances and determine whether one of those two implementations is the one you want.
这篇关于什么时候-XAllowAmbiguousTypes适合？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
