это очень, очень странно в моих глазах.
ел бы получить следующий пример для проверки типа:
{-# 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
тип s (хотя в данном конкретном случае это очевидно, потому что это только частичное приложение):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, например абстракция типа. Я могу подражать этому с уродливымProxy
s, но есть ли какая-то другая особенность GHC Haskell, которая позволяет мне писать что-то вроде этого?