В последнее время я играю с этим типом, который, как я понимаю, является кодировкой свободного дистрибутивного функтора (для тангенциального фона см. этот ответ ):
data Ev g a where
Ev :: ((g x -> x) -> a) -> Ev g a
deriving instance Functor (Ev g)
Экзистенциальный конструктор гарантирует, что я могу потреблять только Ev g
, поставляя полиморфный экстрактор forall x. g x -> x
, и что функциям подъема и опускания свободной конструкции могут быть предоставлены совместимые типы:
runEv :: Ev g a -> (forall x. g x -> x) -> a
runEv (Ev s) f = s f
evert :: g a -> Ev g a
evert u = Ev $ \f -> f u
revert :: Distributive g => Ev g a -> g a
revert (Ev s) = s <$> distribute id
Однако при попытке дать Ev g
экземпляр Distributive
возникает трудность. Учитывая, что Ev g
, в конечном счете, является просто функцией со странным типом аргумента, можно надеяться, что это просто потоковая distribute
для функций (что составляет (??) :: Functor f => f (a -> b) -> a -> f b
от lens , и никак не проверяет тип аргумента) через Ev
обертку:
instance Distributive (Ev g) where
distribute = Ev . distribute . fmap (\(Ev s) -> s)
Это, однако, не работает:
Flap3.hs:95:53: error:
• Couldn't match type ‘x’ with ‘x0’
‘x’ is a rigid type variable bound by
a pattern with constructor:
Ev :: forall (g :: * -> *) x a. ((g x -> x) -> a) -> Ev g a,
in a lambda abstraction
at Flap3.hs:95:44-47
Expected type: (g x0 -> x0) -> a
Actual type: (g x -> x) -> a
• In the expression: s
In the first argument of ‘fmap’, namely ‘(\ (Ev s) -> s)’
In the second argument of ‘(.)’, namely ‘fmap (\ (Ev s) -> s)’
• Relevant bindings include
s :: (g x -> x) -> a (bound at Flap3.hs:95:47)
|
95 | distribute = Ev . distribute . fmap (\(Ev s) -> s)
| ^
Failed, no modules loaded.
GHC возражает против переворачивания экзистенциала, хотя мы ничего не делаем с ним между развёртыванием и перепаковыванием. Единственный выход, который я нашел, - это прибегнуть к unsafeCoerce
:
instance Distributive (Ev g) where
distribute = Ev . distribute . fmap (\(Ev s) -> unsafeCoerce s)
Или, говоря это, возможно, более осторожно:
instance Distributive (Ev g) where
distribute = eevee . distribute . fmap getEv
where
getEv :: Ev g a -> (g Any -> Any) -> a
getEv (Ev s) = unsafeCoerce s
eevee :: ((g Any -> Any) -> f a) -> Ev g (f a)
eevee s = Ev (unsafeCoerce s)
Можно ли обойти эту проблему без unsafeCoerce
? или действительно нет другого пути?
Дополнительные замечания:
Я считаю, Ev
- самый правильный тип, который я могу придать конструкции, хотя я был бы рад оказаться ошибочным. Все мои попытки переместить квантификаторы в другое место привели либо к необходимости unsafeCoerce
где-то еще, либо к evert
и revert
с типами, которые не позволяют их составлять.
Эта ситуация, на первый взгляд, похожа на ситуацию, описанную в этом сообщении в блоге Сэнди Магуайр , которое также заканчивается unsafeCoerce
.
Следующая попытка создания экземпляра Ev g
Representable
может помочь устранить проблему. Как отмечает dfeuer , это не должно быть возможным; неудивительно, что мне пришлось снова использовать unsafeCoerce
:
-- Cf. dfeuer's answer.
newtype Goop g = Goop { unGoop :: forall y. g y -> y }
instance Representable (Ev g) where
type Rep (Ev g) = Goop g
tabulate f = Ev $ \e -> f (Goop (goopify e))
where
goopify :: (g Any -> Any) -> g x -> x
goopify = unsafeCoerce
index (Ev s) = \(Goop e) -> s e
Хотя goopify
, конечно, выглядит тревожно, я думаю, здесь есть причина, по которой это безопасно. Экзистенциальное кодирование означает, что любой e
, который будет передан обернутой функции, обязательно будет полиморфным для экстрактора типа элемента, который специализируется на Any
только потому, что я просил об этом. В таком случае forall x. g x -> x
- разумный тип для e
. Этот танец специализации на Any
только для того, чтобы быстро отменить его с unsafeCoerce
, необходим, потому что GHC заставляет меня избавиться от экзистенциального, сделав выбор. Вот что произойдет, если я пропущу unsafeCoerce
в этом случае:
Flap4.hs:64:37: error:
• Couldn't match type ‘y’ with ‘x0’
‘y’ is a rigid type variable bound by
a type expected by the context:
forall y. g y -> y
at Flap4.hs:64:32-37
Expected type: g y -> y
Actual type: g x0 -> x0
• In the first argument of ‘Goop’, namely ‘e’
In the first argument of ‘f’, namely ‘(Goop e)’
In the expression: f (Goop e)
• Relevant bindings include
e :: g x0 -> x0 (bound at Flap4.hs:64:24)
|
64 | tabulate f = Ev $ \e -> f (Goop e)
| ^
Failed, no modules loaded.
Пролегомена, необходимая для запуска кода здесь:
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
import Data.Distributive
import Data.Functor.Rep
import Unsafe.Coerce
import GHC.Exts (Any)
-- A tangible distributive, for the sake of testing.
data Duo a = Duo { fstDuo :: a, sndDuo :: a }
deriving (Show, Eq, Ord, Functor)
instance Distributive Duo where
distribute u = Duo (fstDuo <$> u) (sndDuo <$> u)