我正在寻找具有以下属性的Haskell类型A(使用异国情调的GHC扩展对我来说很好......):对于所有可遍历的t,以下两种类型是同构的:
forall a. C a => t a -> a
和
t A -> A.
在我的具体情况中,C是以下类:
class Floating a => C a where
fromDouble :: Double -> a
换句话说,我有点想拉全称量化在所有类型的一类ç入式一个,这样一个函数T A - >一个给我回了一个功能都一个.所以我想我正在寻找某种意义上的C级"通用"实例......
我已经考虑了各种花哨的定义一,沿行
newtype A = A (forall b. C b => b)
要么
data A = forall b. C b => A b
要么
newtype A = A (forall t b. (Traversable t, C b) => t b -> b),
要么
data A = FromDouble Double | Plus A A | Tanh A | ...
甚至
data A = A (forall t. Traversable t => t A -> A),
并且它们都可以很容易地成为C类的实例,但它们没有我需要的属性(或者至少我没有看到如何从我上面的任何定义中获取该属性).
在奇怪的日子里,我确信A型根本就不存在,即便是在相信的情况下,我也相信......
...所以任何帮助都将受到高度赞赏!
为了让一些动机我的问题:我扶着严重的爱德华Kmett的广告库为我的神经网络库,并在我的第一次尝试,我用他的Numeric.AD.Rank1.Kahn型自动分化和反向传播.这导致了一个不错的API,但效率低于他的反向模式,不幸的是,我在问题中使用量化来编码可微分函数.
我希望我可以拥有两个世界中最好的 - 一个特定的(抽象)类型加上反向模式效率.
chi*_*chi 12
我们假设A存在这种"通用"类型.
Const () 是可遍历的,因此我们得到了一个同构
forall a. C a => Const () a -> a
-- and
Const () A -> A
即之间(因为Const () a是同构的(),并且() -> b是同构的b)
forall a. C a => a
-- and
A
所以,如果A存在,它必须是同构的forall a. C a => a.
请注意,这是您第一次尝试解决方案 - 如果不满足要求,那么什么都不会.
现在,在你的具体情况下
forall a. C a => a
大致意思是,按C(*)的定义[注意:这里我错误地"忘记了" Floating a超类,整个论证更加脆弱]
forall a. (Double -> a) -> a
这是同构的Double:
iso :: Double -> forall a. (Double -> a) -> a
iso x f = f x
osi :: (forall a. (Double -> a) -> a) -> Double
osi f = f id
证明上述实际上是同构是非平凡的 - 我认为它需要一些参数化,如"免费的递归类型!" .(Yoneda的后果？...评论欢迎!)
所以 - 如果有一个解决方案,C那么它必须是A ~ Double同构的.
(*)我在这里伸展的东西.我不知道如何精确处理Haskell的有限量化,所以我诉诸于使字典显式,即使我猜,它不完全相同.