所以我理解类型的基本代数解释:
Either a b ~ a + b
(a, b) ~ a * b
a -> b ~ b^a
() ~ 1
Void ~ 0 -- from Data.Void
......并且这些关系对于具体类型是正确的,例如Bool,与多态类型相反a.我还知道如何通过根据以下同构转换Church编码,将具有多态类型的类型签名转换为具体类型表示:
(forall r . (a -> r) -> r) ~ a
所以,如果我有:
id :: forall a . a -> a
我知道这并不意味着id ~ a^a,但它实际上意味着:
id :: forall a . (() -> a) -> a
id ~ ()
~ 1
同理:
pair :: forall r . (a -> b -> r) -> r
pair ~ ((a, b) -> r) - > r
~ (a, b)
~ a * b
这让我想到了我的问题.这条规则的"代数"解释是什么:
(forall r . (a -> r) -> r) ~ a
对于每个具体类型的同构,我可以指向一个等价的代数规则,例如:
(a, (b, c)) ~ ((a, b), c)
a * (b * c) = (a * b) * c
a -> (b -> c) ~ (a, b) -> c
(c^b)^a = c^(b * a)
但我不理解代数平等,它类似于:
(forall r . (a -> r) -> r) ~ a
sdc*_*vvc 28
这是身份函子的着名Yoneda引理.
查看这篇文章的可读性介绍,以及任何类别理论教科书了解更多信息.
简而言之,鉴于f :: forall r. (a -> r) -> r您可以申请f id获得a,而相反,x :: a您可以($x)申请获得forall r. (a -> r) -> r.
这些操作是相反的.证明:
显然($x) id == x.我会证明这一点
($(f id)) == f,
因为功能是当他们在所有参数等于平等,让我们x :: a -> r和显示,
($(f id)) x == f x 即
x (f id) == f x.
由于f是多态的,它起着自然的转变作用; 这是以下的自然图f:
f_A
Hom(A, A) ? A
(x.) ? ? x
Hom(A, R) ? R
f_R
所以x . f == f . (x.).
堵塞身份,(x . f) id == f x.QED
cop*_*kin 17
(为清楚起见重写)
您的问题似乎有两个部分.一个暗示并且正在询问代数解释是什么forall,另一个是询问cont/Yoneda转换,sdcvvc的答案已经很好地涵盖了.
我会试着解决你的代数解释forall.你提到的A -> B是,B^A但我想进一步将其扩展到B * B * B * ... * B(|A|时间).虽然我们确实将取幂作为重复乘法的符号,但是有一个更灵活的表示法?(大写Pi)代表任意索引产品.Pi有两个组成部分:我们想要乘以的值的范围,以及我们乘以的表达式.例如,在值级别,您可以将阶乘函数表示为fact i = ? [1..i] (?x -> x).
回到类型世界,我们可以将A -> B ~ B^A对应中的取幂运算符视为Pi : B^A ~ ? A (?_ -> B). 这说明我们正在定义s的一个A产品B,这样Bs就不能依赖于A我们选择的特定产品.当然,它等同于普通指数,但它让我们向上移动到存在依赖性的情况.
在最一般的情况下,我们得到依赖类型,就像你在Agda或Coq中看到的那样:在Agda语法中,replicate : Bool -> ((n : Nat) -> Vec Bool n)是Pi类型的一种可能的应用,可以更明确地表达为replicate : Bool -> ? Nat (Vec Bool)或者进一步表达replicate : ? Bool (?_ -> ? Nat (Vec Bool)).
请注意,正如您可能从底层代数中所期望的那样,您可以?将replicate上面定义中的两个s 融合到?域的笛卡尔积上的单个范围中:? Bool (\_ -> ? Nat (Vec Bool))等同于? (Bool, Nat) (?(_, n) -> Vec Bool n)它在"值级"上的相同.从类型理论的角度来看,这简直不了解.
我确实意识到你的问题是关于多态性的,所以我将继续讨论依赖类型,但它们是相关的:forall在Haskell中大致相当于?一个域类型(种类)的域名,*.实际上,多态性的类似函数的行为可以直接在GHC核心中观察到,GHC核心将它们命名为大写lambda(Λ).因此,类似的多态类型forall a. a -> a实际上只是? * (? a -> (a -> a))(现在使用Λ表示法我们区分类型和值),这可以扩展到(Bool -> Bool, Int -> Int, () -> (), (Int -> Bool) -> (Int -> Bool), ...)每种可能类型的无限产品.类型变量的实例化只是从*-ary产品中突出出合适的元素(或应用类型函数).
现在,对于我在这个答案的原始版本中错过的重要部分:参数化.参数化可以用几种不同的方式来描述,但我所知道的(观察类型为关系,或类别理论中的(di)自然性)中没有一个真正具有非常代数的解释.但是,就我们的目的而言,它归结为一些相当简单的东西:你不能模式匹配*.我知道GHC允许你在类型级别使用类型系列执行此操作,但是*在执行此操作时,您只能覆盖有限的一部分,因此必须始终指定类型系列未定义的点.
从多态性的角度来看,这意味着F我们编写的任何类型函数? * F必须是常量(即,完全忽略它是多态的类型)或者通过未更改的类型传递.因此,? * (? _ -> B)有效是因为它忽略了它的参数,并且对应于forall a. B.另一种情况是? * (? x -> Maybe x),它对应于forall a. Maybe a,它不会忽略类型参数,而只是"传递它".因此? A,具有不相关域A(例如何时A = *)的那个可以被视为更多的A索引交叉(在索引的所有实例中选择公共元素),而不是产品.
至关重要的是,在价值层面,参数规则可以防止任何可能暗示类型比实际更大的有趣行为.因为我们没有typecase,所以我们无法forall a. B根据a实例化的内容构造一个不同类型的值.因此,虽然类型在技术上是一个函数* -> B,但它始终是一个常数函数,因此相当于单个值B.使用?解释,它确实相当于s 的无限*乘积B,但这些B值必须始终相同,因此无限乘积实际上与单个一样大B.
类似地,虽然? * (? x -> (x -> x))(aka forall a. a -> a)在技术上等同于函数的无限产品,但这些函数都不能检查类型,因此所有函数都被约束为只返回它们的输入值而不是像(+1) : Int -> Int实例化那样做任何有趣的业务Int.因为只有一个(假设一个总语言)函数不能检查其参数的类型但必须返回相同类型的值,因此无限乘积与单个值一样大.
现在,关于你的直接问题(forall r . (a -> r) -> r) ~ a.首先,让我们~更正式地表达您的运营商.它真的是同构,所以我们需要来回两个函数,以及它们反转的论证.
data Iso a b = Iso
{ to :: a -> b
, from :: b -> a
-- proof1 :: forall x. to (from x) == x
-- proof2 :: forall x. from (to x) == x
}
现在我们用更正式的语言表达你原来的问题.你的问题等于构建以下术语(不可预测,因此GHC遇到麻烦,但我们会幸存下来)类型:
forall a. Iso (forall r. (a -> r) -> r) a
使用我之前的术语,相当于? * (? a -> Iso (? * (? r -> ((a -> r) -> r))) a).我们再次拥有一个无法检查其类型参数的无限产品.通过手工操作,我们可以争辩说,考虑参数性规则的唯一可能的值(其他两个证明自动得到尊重)to和from是($ id)和flip id.
如果这感觉不满意,可能是因为代数解释forall并没有真正为证明添加任何东西.它实际上只是普通的旧式理论,但我希望我能够提供一些比Yoneda形式更不具有某种意义的东西.值得注意的是,我们实际上并不需要使用参数化来编写proof1和proof2更高版本.Parametricity只有进入时,我们想声明的是,图片($ id)和flip id是我们唯一的选项to和from(我们不能在阿格达或勒柯克证明,因为这个原因).
为了(试图)回答实际问题(这比提出的更广泛问题的答案不那么有趣),问题因为"类型错误"而形成错误
Either ~ (+)
(,) ~ (*)
(->) b ~ flip (^)
() ~ 1
Void ~ 0
这些都将类型映射到整数,并在自然函数上键入构造函数.从某种意义上说,你有一个从类型类别到自然类别的仿函数.在另一个方向,你"忘记"的东西,因为类型保留代数结构,而自然抛弃它.即,Either () ()你可以得到一个独特的自然,但鉴于自然,你可以得到很多类型.
但这是不同的:
(forall r . (a -> r) -> r) ~ a
它将一种类型映射到另一种类型!它不是上述仿函数的一部分.它只是类型范畴内的同构.那么让我们给出一个不同的符号,<=>
现在我们有
(forall r . (a -> r) -> r) <=> a
现在你注意到我们不仅可以向nats和箭头发送类型到箭头,还可以向其他同构发送一些同构:
(a, (b, c)) <=> ((a, b), c) ~ a * (b * c) = (a * b) * c
但这里有一些微妙的东西.从某种意义上说,后者对同构是正确的,因为代数同一性是正确的.这就是说后者中的"同构"仅仅意味着这两种类型在我们的函子形象下是等价的.
前同构我们需要直接证明,这是我们开始得到基本问题的地方 - 给我们的nats的函子,forall r.映射到什么？但答案是,forall r.既不是类型,也不是类型之间有意义的箭头.
通过引入forall,我们已经从一阶类型转移.有没有理由期望FORALL 应该适合我们上面的函子,而事实上,它没有.
所以我们可以像其他人一样探索为什么同构存在(这本身就很有趣) - 但是这样做我们已经放弃了问题的代数核心.一个问题可以回答,我想,是,给高阶类型和构造的类别为他们之间的箭头,什么是没有意义的函子来？
编辑:所以现在我有另一种方法,它显示了为什么添加多态会使事情变得疯狂.我们首先提出一个更简单的问题 - 给定的多态类型是否具有零或多于零的居民？这就是类型居住问题,并且通过Curry-Howard来解决修改的可实现性问题,因为它与在某个逻辑中的公式是否可以在适当的计算模型中实现相同.现在正如该页面所解释的那样,这在简单类型的lambda演算中是可判定的,但是PSPACE完全.但是,一旦我们转向更复杂的东西,例如通过添加多态性并转到System F,那么它就变得不可判定了!
所以,如果我们无法决定一个任意类型是否有人居住,那么我们显然无法决定它拥有多少居民!