haskell - -XAllowAmbigouslyTypes 什么时候合适？

Question

我最近发布了 question关于syntactic-2.0关于 share 的定义。我已经在 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

但是，GHC 7.8 想要 -XAllowAmbiguousTypes使用该签名进行编译。或者，我可以替换 fi与

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

这是SyntacticN上的fundep隐含的类型。这使我可以避免延期。当然这是

• 一个非常长的类型，可以添加到已经很大的签名中
• 手动导出很烦人
• 由于基金的原因没有必要

我的问题是:

1. 这是 -XAllowAmbiguousTypes 的可接受使用吗？ ？
2. 一般来说，什么时候应该使用这个扩展？一个答案here建议“这几乎从来都不是一个好主意”。

3. 虽然我读过the docs ，我仍然无法确定约束是否不明确。具体来说，请考虑 Data.Syntropic.Sugar 中的此函数:

   sugarSym :: (sub :<: AST sup, ApplySym sig fi sup, SyntacticN f fi) 
            => sub sig -> f
   sugarSym = sugarN . appSym
   

   在我看来fi (可能是 sup )在这里应该是不明确的，但它在没有扩展名的情况下进行编译。为什么是sugarSym明确同时 share是？自 share是sugarSym的应用程序，share约束全部直接来自 sugarSym .

Answer 1

我没有看到任何已发布的语法版本的 sugarSym 签名使用这些确切的类型名称，因此我将使用 the development branch at commit 8cfd02^ ，仍然使用这些名称的最后一个版本。

那么，为什么 GHC 会提示类型签名中的 fi 而不是 sugarSym 呢？您链接到的文档解释说，如果类型没有出现在约束的右侧，则该类型是不明确的，除非约束使用函数依赖项从其他非二义类型推断出其他不明确的类型。因此，让我们比较两个函数的上下文并查找函数依赖性。

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

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

现在让我们看看糖。我注意到的第一件事是编译器不是提示不明确的类型，而是提示重叠的实例:

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

所以，如果我没看错的话，并不是说 GHC 认为你的类型不明确，而是在检查你的类型是否不明确时，GHC 遇到了一个不同的、单独的问题。然后它告诉您，如果您告诉 GHC 不要执行歧义性检查，它就不会遇到该单独的问题。这解释了为什么启用AllowAmbigouslyTypes 可以让您的代码进行编译。

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

我怀疑 Syntropic 是用 OverlappingInstances 编译的。并看着the code ，确实如此。

经过一点实验，当很明显一个实例比另一个实例更通用时，GHC 似乎可以处理重叠实例:

{-# 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])

但是当两个实例明显都不比另一个更适合时，GHC 不接受重叠实例:

{-# 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])

您的类型签名使用 SyntropicN (a -> (a -> b) -> b) fi，并且既不是 SyntropicN f fi 也不是 SyntropicN (a -> f) (AST sym (Full ia) -> fi) 比另一个更合适。如果我将类型签名的该部分更改为 SyntropicN a fi 或 SyntropicN (a -> (a -> b) -> b) (AST sym (Full ia) -> fi) ，GHC 不再提示重叠。

如果我是你，我会查看 the definition of those two possible instances并确定这两种实现之一是否是您想要的。