В последнее время я играю с этим типом, который, как я понимаю, является кодировкой свободного дистрибутивного функтора (для тангенциального фона см. этот ответ ):
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)