在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

我得知它可能无法推断和检查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功能让我写这样的东西吗？

Answer 1

这是设计使然。Proxy目前似乎无法使用s：https: //ghc.haskell.org/trac/ghc/ticket/15119。

2019 年 7 月编辑：现在有一个GHC 提案！