GHC Haskell 中的类型抽象答案

【问题标题】：Type abstraction in GHC HaskellGHC Haskell 中的类型抽象
【发布时间】：2018-05-03 15:59:19
【问题描述】：

我希望得到以下示例来进行类型检查：

{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilies           #-}

module Foo where

f :: Int -> (forall f. Functor f => Secret f) -> Int
f x _ = x

g :: (forall f. Functor f => Secret f) -> Int
g = f 4

type family Secret (f :: * -> *) :: * where
  Secret f = Int

我知道可能无法推断和检查 gs 类型（尽管在这种特定情况下很明显，因为它只是一个部分应用程序）：Secret 不是单射的，没有办法告诉Functor 实例应该期望的编译器。因此，它失败并显示以下错误消息：

    • Could not deduce (Functor f0)
      from the context: Functor f
        bound by a type expected by the context:
                  forall (f :: * -> *). Functor f => Secret f
        at src/Datafix/Description.hs:233:5-7
      The type variable ‘f0’ is ambiguous
      These potential instances exist:
        instance Functor IO -- Defined in ‘GHC.Base’
        instance Functor Maybe -- Defined in ‘GHC.Base’
        instance Functor ((,) a) -- Defined in ‘GHC.Base’
        ...plus one other
        ...plus 9 instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the expression: f 4
      In an equation for ‘g’: g = f 4
    |
233 | g = f 4
    |     ^^^

因此需要程序员的一些指导，如果我可以这样写g，那将很容易被接受：

g :: (forall f. Functor f => Secret f) -> Int
g h = f 4 (\\f -> h @f)

\\ 是 System Fw 的大 lambda 的假设语法，即类型抽象。我可以用丑陋的Proxys 来模拟这个，但是还有其他一些 GHC Haskell 功能可以让我写这样的东西吗？

【问题讨论】：

f 的声明中出现歧义错误。你打开了AllowAmbiguousTypes 吗？
是的，我愿意。给我一点时间来编辑带有所有必要扩展名的问题。

标签： haskell type-families existential-type system-f

【解决方案1】：

这可能是 GHC 错误。我看不出这种 GHC 行为有什么意义。

这个问题与类型族无关，但似乎是由模棱两可的类型和类型类约束引起的。

这是针对同一问题的 MCVE。

{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TypeApplications       #-}

class C a where
   getInt :: Int

instance C Char where
   getInt = 42

f :: (forall a. C a => Int) -> Bool
f x = even (x @ Char)

g :: (forall a. C a => Int) -> Bool
-- g = f               -- fails
-- g h = f h           -- fails
-- g h = f getInt      -- fails
g _ = f 42             -- OK

似乎f 不能用任何实际利用约束的参数调用。

【讨论】：

【解决方案2】：

这是设计使然。现在似乎没有办法使用Proxys：https://ghc.haskell.org/trac/ghc/ticket/15119。

2019 年 7 月编辑：现在有一个 GHC proposal for this！

【讨论】：

我不明白为什么这不被认为是一个错误。如果不允许模棱两可的类型，我不会。但是由于现在可以打开模棱两可的类型，我看不出代码有什么问题。我认为这是 GHC 的一个非常奇怪的技术限制，充其量。我想知道推理算法中是否有一些深层原因导致类型检查失败，或者这只是一个事件。哦，好吧。
我猜你不能让它在一般情况下工作，而不是尝试一些具体和明显的情况来保持推理简单合理。如果这可行，我们将对其他一些更难以推断的示例进行相同的讨论。问题是，我们在哪里停止类型推断中的这种临时黑客攻击？
可能是这样，但 trac 讨论不支持这种观点。它只是说“它是模棱两可的，因此 GHC 无法处理它”，当仅凭这个原因还不够时，因为 GHC 接受 f 就好了，即使它有一个模棱两可的类型。事实上，trac 讨论似乎错误地指出，你不能写 f。无论类型检查算法接受x :: T ; x = expr（对于某些T,expr）但拒绝x :: T ; x = expr ; y :: T ; y = x，在我眼中都是非常非常奇怪的。