在没有不安全的情况下杂耍存在 [英] Juggling existentials without unsafeCoerce
问题描述
最近我一直在使用这种类型,我将其理解为自由分布仿函数的编码(有关其切线背景,请参见
Lately I have been playing with this type, which I understand to be an encoding of the free distributive functor (for tangential background on that, see this answer):
data Ev g a where
Ev :: ((g x -> x) -> a) -> Ev g a
deriving instance Functor (Ev g)
存在构造函数可确保我只能通过提供多态提取器forall x. g x -> x
来使用Ev g
,并且可以为自由构造的提升和降低功能指定兼容类型:
The existential constructor ensures I can only consume an Ev g
by supplying a polymorphic extractor forall x. g x -> x
, and that the lift and lower functions of the free construction can be given compatible types:
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
However, there is a difficulty upon trying to give Ev g
a Distributive
instance. Given that Ev g
is ultimately just a function with a weird argument type, one might hope that just threading distribute
for functions (which amounts to (??) :: Functor f => f (a -> b) -> a -> f b
from lens, and doesn't inspect the argument type in any way) through the Ev
wrapper:
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
:
GHC objects to rewrapping the existential, even though we do nothing untoward with it between unwrapping and rewrapping. The only way out I found was resorting to unsafeCoerce
:
instance Distributive (Ev g) where
distribute = Ev . distribute . fmap (\(Ev s) -> unsafeCoerce s)
或者,以一种更为谨慎的方式进行拼写:
Or, spelling it in a perhaps more cautious manner:
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
的情况下解决此问题?还是真的没有其他方法?
Is it possible to get around this problem without unsafeCoerce
? or there truly is no other way?
其他说明:
-
我相信
Ev
是我可以赋予结构的最正确的类型,尽管我很乐意被证明是错误的.我所有将量词移动到其他地方的尝试都导致需要unsafeCoerce
到其他地方,或者导致evert
和revert
的类型不允许它们组成.
I believe
Ev
is the most correct type I can give to the construction, though I would be happy to be proved wrong. All my attempts to shift the quantifiers elsewhere lead either to needingunsafeCoerce
somewhere else or toevert
andrevert
having types that don't allow them to be composed.
这种情况乍看之下,类似于Sandy Maguire在此博客文章中描述的情况,最后也坚持使用unsafeCoerce
.
This situation looks, at first glance, similar to the one described in this blog post by Sandy Maguire, which ends up sticking with unsafeCoerce
as well.
以下为Ev g
赋予Ev g
实例的方法可能会使问题更加明显. 如所指出的那样,这实际上是不可能的.毫不奇怪,我不得不再次使用unsafeCoerce
:
The following take at giving Ev g
a Representable
instance might put the problem into sharper relief. As dfeuer notes, this isn't really supposed to be possible; unsurprisingly, I had to use unsafeCoerce
again:
-- 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
,就会发生这种情况:
While goopify
sure looks alarming, I think there is a case for it being safe here. The existential encoding means any e
that gets passed to the wrapped function will necessarily be an extractor polymorphic on the element type, that gets specialised to Any
merely because I asked for that to happen. That being so, forall x. g x -> x
is a sensible type for e
. This dance of specialising to Any
only to promptly undo it with unsafeCoerce
is needed because GHC forces me to get rid of the existential by making a choice. This is what happens if I leave out the unsafeCoerce
in this case:
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.
Prolegomena需要在此处运行代码:
Prolegomena needed to run the code here:
{-# 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)
推荐答案
danidiaz和dfeuer的建议使我采用了更简洁的编码,尽管unsafeCoerce
仍然是必需的:
The suggestions by danidiaz and dfeuer have led me to a tidier encoding, though unsafeCoerce
is still necessary:
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
import Unsafe.Coerce
import GHC.Exts (Any)
import Data.Distributive
import Data.Functor.Rep
-- Px here stands for "polymorphic extractor".
newtype Px g = Px { runPx :: forall x. g x -> x }
newtype Ev g a = Ev { getEv :: Px g -> a }
deriving Functor
runEv :: Ev g a -> (forall x. g x -> x) -> a
runEv s e = s `getEv` Px e
evert :: g a -> Ev g a
evert u = Ev $ \e -> e `runPx` u
revert :: Distributive g => Ev g a -> g a
revert (Ev s) = (\e -> s (mkPx e)) <$> distribute id
where
mkPx :: (g Any -> Any) -> Px g
mkPx e = Px (unsafeCoerce e)
instance Distributive (Ev g) where
distribute = Ev . distribute . fmap getEv
instance Representable (Ev g) where
type Rep (Ev g) = Px g
tabulate = Ev
index = getEv
在我最初的Ev
公式中,x
变量被普遍量化;我只是将其伪装成功能箭头后面的存在.尽管这种编码可以在不使用unsafeCoerce
的情况下编写revert
,但它将负担转移到了实例实现上.在这种情况下,直接使用通用量化最终会更好,因为它将魔术集中在一个地方.
The x
variable in my original formulation of Ev
was, at heart, being universally quantified; I had merely disguised it as an existential behind a function arrow. While that encoding makes it possible to write revert
without unsafeCoerce
, it shifts the burden to the instance implementations. Directly using universal quantification is ultimately better in this case, as it keeps the magic concentrated in one place.
这里的unsafeCoerce
技巧与问题中的tabulate
基本上相同:distribute id :: Distributive g => g (g x -> x)
中的x
专用于Any
,然后在fmap
下立即撤消了专项,使用unsafeCoerce
.我相信这个技巧是安全的,因为我可以完全控制unsafeCoerce
的内容.
The unsafeCoerce
trick here is essentially the same demonstrated with tabulate
in the question: the x
in distribute id :: Distributive g => g (g x -> x)
is specialised to Any
, and then the specialisation is immediately undone, under the fmap
, with unsafeCoerce
. I believe the trick is safe, as I have sufficient control over what is being fed to unsafeCoerce
.
至于要摆脱unsafeCoerce
,我真的看不到办法.问题的一部分是,我似乎需要某种形式的强制性类型,因为unsafeCoerce
技巧最终等于将forall x. g (g x -> x)
转换为g (forall x. g x -> x)
.为了进行比较,我可以使用强制性类型功能的子集编写一个模糊的类似(如果更简单)的场景,该子集将落入有争议的ExplicitImpredicativeTypes
扩展的范围内(请参阅
As for getting rid of unsafeCoerce
, I truly can't see a way. Part of the problem is that it seems I would need some form of impredicative types, as the unsafeCoerce
trick ultimately amounts to turning forall x. g (g x -> x)
into g (forall x. g x -> x)
. For the sake of comparison, I can write a vaguely analogous, if much simpler, scenario using the subset of the impredicative types functionality that would fall under the scope of the mooted ExplicitImpredicativeTypes
extension (see GHC ticket #14859 and links therein for discussion):
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE RankNTypes #-}
newtype Foo = Foo ([forall x. Num x => x] -> Int)
testFoo :: Applicative f => Foo -> f Int
testFoo (Foo f) = fmap @_ @[forall x. Num x => x] f
$ pure @_ @[forall x. Num x => x] [1,2,3]
GHCi> :set -XImpredicativeTypes
GHCi> :set -XTypeApplications
GHCi> testFoo @Maybe (Foo length)
Just 3
但是,
distribute id
比[1,2,3]
棘手.在id :: g x -> g x
中,我要保持量化的类型变量出现在两个位置,其中一个是distribute
的第二个类型参数((->) (g x)
函子).至少在我未经训练的眼睛看来,这完全是棘手的.
distribute id
, however, is thornier than [1,2,3]
. In id :: g x -> g x
, the type variable I'd like to keep quantified appears in two places, with one of them being the second type argument to distribute
(the (->) (g x)
functor). To my untrained eye at least, that looks utterly intractable.
这篇关于在没有不安全的情况下杂耍存在的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!