haskell - AllowAmbiguousTypes和命题相等性: what's going on here?

因此，前几天我想出了如何编写此函数(需要base-4.7.0.0或更高版本):

{-# LANGUAGE ScopedTypeVariables, TypeOperators, GADTs #-}

import Data.Typeable

-- | Test dynamically whether the argument is a 'String', and boast of our
-- exploit if so.
mwahaha :: forall a. Typeable a => a -> a
mwahaha a = case eqT :: Maybe (a :~: String) of
              Just Refl -> "mwahaha!"
              Nothing -> a

因此，我无所适从，决定尝试使用它来编写一个测试其参数类型是否为Show实例的函数。如果我正确理解的话，这是行不通的，因为TypeRep仅适用于单态类型。因此，此定义自然无法进行类型检查:

isShow :: forall a b. (Typeable a, Typeable b, Show b) => a -> Bool
isShow a = case eqT :: Maybe (a :~: b) of
             Just Refl -> True
             Nothing -> False

{-
/Users/luis.casillas/src/scratch.hs:10:11:
    Could not deduce (Typeable b0)
      arising from the ambiguity check for ‘isShow’
    from the context (Typeable a, Typeable b, Show b)
      bound by the type signature for
                 isShow :: (Typeable a, Typeable b, Show b) => a -> Bool
      at /Users/luis.casillas/src/scratch.hs:10:11-67
    The type variable ‘b0’ is ambiguous
    In the ambiguity check for:
      forall a b. (Typeable a, Typeable b, Show b) => a -> Bool
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In the type signature for ‘isShow’:
      isShow :: forall a b. (Typeable a, Typeable b, Show b) => a -> Bool
-}

但是请注意消息To defer the ambiguity check to use sites, enable AllowAmbiguousTypes。如果启用该编译指示，则定义类型会检查，但是...

{-# LANGUAGE ScopedTypeVariables, TypeOperators, GADTs #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

import Data.Typeable

isShow :: forall a b. (Typeable a, Typeable b, Show b) => a -> Bool
isShow a = case eqT :: Maybe (a :~: b) of
             Just Refl -> True
             Nothing -> False

{- Typechecks, but...

>>> isShow 5
False

>>> isShow (id :: String -> String)
False
-}

这里发生了什么？编译器为b选择哪种类型？它是Skolem类型的变量àla ExistentialTypes吗？

哦，对，我只是问了一个问题，很快就想出了答案:

whatsTheTypeRep :: forall a b. (Typeable a, Typeable b, Show b) => a -> TypeRep
whatsTheTypeRep a = typeRep (Proxy :: Proxy b)

{-
>>> whatsTheTypeRep 5
()

>>> isShow ()
True
-}

我仍然对听到这里发生的事情感兴趣。这是默认规则吗？

最佳答案

打开-Wall，您将得到答案:)

<interactive>:50:11: Warning:
    Defaulting the following constraint(s) to type ‘()’
      (Typeable b0)
        arising from the ambiguity check for ‘isShow’
        at <interactive>:50:11-67
      (Show b0)
        arising from the ambiguity check for ‘isShow’
        at <interactive>:50:11-67
    In the ambiguity check for:
      forall a b. (Typeable a, Typeable b, Show b) => a -> Bool
    In the type signature for ‘isShow’:
      isShow :: forall a b. (Typeable a, Typeable b, Show b) => a -> Bool

(是的，这是默认规则)

关于haskell - AllowAmbiguousTypes和命题相等性: what's going on here?，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/27008046/