GHC 中的类型抽象 Haskell

Question

我很想获得以下示例以进行类型检查：

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

我知道它可能无法推断和检查 g 的类型（即使在这种特定情况下它很明显，因为它只是一个部分应用程序）：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 特性让我写这样的东西？

Answer 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 不能用实际利用约束的任何参数调用。

Answer 2

这是设计使然。似乎暂时无法使用 Proxys：https://ghc.haskell.org/trac/ghc/ticket/15119.

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

GHC 中的类型抽象 Haskell

Type abstraction in GHC Haskell

haskell

existential-type

type-families

system-f