我希望对以下示例进行类型检查:
{-# 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 的假设语法,即类型抽象。我可以用丑陋的 Proxy 来模拟这个,但是还有其他一些 GHC Haskell 功能可以让我写这样的东西吗?
最佳答案
这可能是 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
。
关于haskell - GHC Haskell 中的类型抽象,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/50159349/