-XAllowAmbiguousTypes 什么时候合适? [英] When is -XAllowAmbiguousTypes appropriate?

问题描述

我最近发布了一个关于 syntactic-2.0 关于share 的定义.我在 GHC 7.6 中使用过这个:

{-# LANGUAGE GADTs、TypeOperators、FlexibleContexts #-}导入数据.句法导入 Data.Syntactic.Sugar.BindingT数据让一个地方Let :: Let (a :-> (a -> b) :-> Full b)分享 :: (让 :<: sup,sup ~ 域 b, sup ~ 域 a,句法a, 句法b,句法 (a -> b)，句法N (a -> (a -> b) -> b)f)=>->(a -> b) ->乙分享 = SugarSym 让

然而，GHC 7.8 希望 -XAllowAmbiguousTypes 使用该签名进行编译.或者，我可以用

替换 fi

(ASTF sup (Internal a) -> AST sup ((Internal a) :-> Full (Internal b)) -> ASTF sup (Internal b))

这是fundep在SyntacticN上隐含的类型.这使我可以避免扩展.当然是

• 要添加到已经很大的签名中的很长的类型
• 手动推导很烦
• 由于资金原因不必要

我的问题是:

1. 这是对 -XAllowAmbiguousTypes 的可接受使用吗?
2. 一般来说，什么时候应该使用这个扩展?此处的答案表明几乎从来都不是一个好主意".

3. 虽然我读过 文档，我仍然无法确定约束是否含糊不清.具体来说，考虑 Data.Syntactic.Sugar 中的这个函数:

   sugarSym :: (sub :<: AST sup, ApplySym sig fi sup, SyntacticN f fi)=>子签名 ->F糖符号 = 糖N.应用符号

   在我看来 fi(可能还有 sup)在这里应该是不明确的，但它编译时没有扩展.为什么 sugarSym 是明确的，而 share 是?由于share是sugarSym的应用，所以share约束都直接来自sugarSym.

解决方案

我没有看到任何已发布版本的语法，其 sugarSym 的签名使用那些确切的类型名称，所以我将使用提交 8cfd02^ 处的开发分支，最后一个版本仍然使用这些名称.

那么，为什么 GHC 会抱怨类型签名中的 fi 而不是 sugarSym 的?您链接到的文档解释说，如果某个类型没有出现在约束的右侧，则该类型是不明确的，除非该约束使用函数依赖项从其他非歧义类型中推断出其他歧义类型.那么让我们比较一下这两个函数的上下文，寻找函数依赖.

class ApplySym sig f sym |符号符号 ->f，f-＞符号符号class SyntacticN f 内部 |f->内部的SugarSym :: ( sub :<: AST sup, ApplySym sig fi sup, 句法N f fi)=>子签名 ->F分享 :: ( 让 ::<: sup, sup ~ 域 b, sup ~ 域 a, 句法 a, 句法 b, 句法 (a -> b), SyntacticN (a -> (a -> b) -> b) fi)=>->(a -> b) ->乙

所以对于 sugarSym，非歧义类型是 sub、sig 和 f，从那些我们应该能够遵循函数依赖关系以消除上下文中使用的所有其他类型的歧义，即 sup 和 fi.事实上，f ->SyntacticN 中的内部 函数依赖使用我们的 f 来消除我们的 fi 的歧义，然后 f ->ApplySym 中的 sig sym 函数依赖使用我们新消歧义的 fi 来消歧 sup(和 sig，这已经是明确的).这就解释了为什么 sugarSym 不需要 AllowAmbiguousTypes 扩展.

现在让我们看看sugar.我注意到的第一件事是编译器不是抱怨类型不明确，而是抱怨实例重叠:

SyntacticN b fi 的重叠实例由共享"的歧义检查引起匹配给定(或它们的超类):(SyntacticN (a -> (a -> b) -> b) fi1)匹配实例:实例 [重叠确定](句法 f，域 f ~ sym，fi ~ AST sym (Full (Internal f))) =>句法N f fi-- 在‘Data.Syntactic.Sugar’中定义实例[重叠确定](句法a，域a~sym，ia~内部a，句法N f fi) =>SyntacticN (a -> f) (AST sym (Full ia) -> fi)-- 在‘Data.Syntactic.Sugar’中定义(选择取决于‘b, fi’的实例化)要推迟使用网站的歧义检查，请启用 AllowAmbiguousTypes

所以如果我没看错的话，并不是 GHC 认为您的类型有歧义，而是在检查您的类型是否有歧义时，GHC 遇到了一个不同的、单独的问题.然后它告诉你，如果你告诉 GHC 不要执行歧义检查，它就不会遇到那个单独的问题.这解释了为什么启用 AllowAmbiguousTypes 允许您的代码编译.

然而，重叠实例的问题仍然存在.GHC 列出的两个实例(SyntacticN f fi 和 SyntacticN (a -> f) ...)确实彼此重叠.奇怪的是，第一个似乎应该与任何其他实例重叠，这很可疑.[overlap ok] 是什么意思?

我怀疑 Syntactic 是用 OverlappingInstances 编译的.查看代码，确实如此.>

稍微试验一下，当很明显一个实例比另一个更通用时，GHC 似乎可以处理重叠实例:

{-# LANGUAGE FlexibleInstances, OverlappingInstances #-}类 Foo a 在哪里whichOne :: a ->细绳实例 Foo a wherewhichOne _ = "a"实例 Foo [a] 其中whichOne _ = "[a]"-- |-->>>主要的-  [一个]主要:: IO()main = putStrLn $ whichOne (undefined :: [Int])

但是当两个实例显然都不比另一个更适合时，GHC 不适用于重叠实例:

{-# LANGUAGE FlexibleInstances, OverlappingInstances #-}类 Foo a 在哪里whichOne :: a ->细绳instance Foo (f Int) where -- 这是改变的行whichOne _ = "f Int"实例 Foo [a] 其中whichOne _ = "[a]"-- |-->>>主要的-- 错误:Foo [Int] 的重叠实例主要:: 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:

1. Is this an acceptable use of -XAllowAmbiguousTypes?
2. In general, when should this extension be used? An answer here suggests "it is almost never a good idea".

3. 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 . appSym
   

   It appears to me that fi (and possibly sup) should be ambiguous here, but it compiles without the extension. Why is sugarSym unambiguous while share is? Since share is an application of sugarSym, the share constraints all come straight from sugarSym.

解决方案

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屋！