问题描述
Control.Category.Constrained 是一个非常有趣的项目，它介绍了笛卡尔封闭类别的类- Curry .
但是，我不明白为什么我们会想到所有允许 curry 和 uncurry 的笛卡尔封闭类别( Hom(X * Y，Z)≅Hom(X，Z ^ Y)的范畴论).维基百科说，此类属性仅适用于本地小的笛卡尔封闭类别.在此帖子下，许多人认为 Hask 本身在本地并不小(另一方面，每个人都说 Hask 不是笛卡尔封闭类别，我认为这是纯粹而无趣的形式主义.
Yet, I do not see why we think of all cartesian closed categories which allow curry and uncurry (Hom(X * Y, Z) ≅ Hom(X, Z^Y) in terms of category theory). Wikipedia says that such property holds only for locally small cartesian closed categories. Under this post many people suggest that Hask itself is not locally small (on the other hand, everyone says that Hask is not a cartesian closed category, which I reckon to be pure and uninteresting formalism).
在上的此帖子中Math.SE 假设所有类别在本地都较小.但这是从我们讨论属性的数学观点给出的.我想知道为什么我们决定专注于 curry 和 uncurry 作为 Curry 的方法.是因为几乎每个了解Haskell的人都知道这些功能吗?还是还有其他原因?
In this post on Math.SE speaks on assuming all categories are locally small. But it is given from a mathematical point of view where we discuss properties. I would like to know why we decided to concentrate on curry and uncurry as Curry’s methods. Is it because pretty much everyone who knows Haskell also knows these functions? Or is there any other reason?
推荐答案
作为图书馆的作者，我可以自信地回答，答案是是:这是因为 curry 和 uncurry 的建立良好Haskell本地语言的一部分. constrained-categories 从未打算在某种意义上从根本上改变Haskell和/或使其在数学上更可靠，而只是巧妙地概括了现有的类层次结构-主要是为了允许定义函子等.被赋予 Prelude.Functor 实例.
As the library author I can answer that with confidence and the answer is yes: it is because curry and uncurry are well-established part of the Haskell vernacular. constrained-categories was never intended to radically change Haskell and/or make it more mathematically solid in some sense, but rather to subtly generalise the existing class hierarchies – mostly to allow defining functors etc. that couldn't be given Prelude.Functor instances.
坦率地说， Curry 是否可以用局部小化形式化，我实在不知道.我也不确定是否可以在Haskell库的上下文中有意义地讨论该方面以及其他数学基础"方面.这只是Haskell是一种非全部语言的事实，是的，这意味着几乎所有公理都可以受到某些 undefined 攻击的破坏.但是我也不认为这是一个问题.许多人似乎将Haskell视为一种不可思议的山谷:在现实应用中使用时过于严格，但没有任何证据可以正确证明.我恰恰相反:Haskell具有足够强大的类型系统，可以表达对实际应用有用的数学思想，而不会使其价值语义深深陷入在现实世界中实际使用的基础.(即，您不会持续花费数周的时间来证明显然是……"定理.我在看着您，考克... )
而不是写100％严格的证明，我们尽可能缩小类型的范围，然后使用QuickCheck来查看数学上通常要求的通常有效的.
Whether Curry could be formalised in terms of local smallness I frankly don't know. I'm also not sure whether that and other "maths foundations" aspects can even be meaningfully discussed in the context of a Haskell library. It's just a fact that Haskell is a non-total language, and yes, that means just about any axiom can be thwarted by some undefined attack. But I also don't really see that as a problem. Many people seem to think of Haskell as a sort of uncanny valley: too restrictive for use in real-world applications, yet nothing can be proved properly. I see it exactly the other way around: Haskell has a sufficiently powerful type system to be able to express the mathematical ideas that are useful for real-world applications, without getting its value semantics caught up too deep in the underlying foundations to be practical to actually use in the real world. (I.e., you don't constantly spend weeks proving some "obviously it's true that..." theorem. I'm looking at you, Coq...)
Instead of writing 100% rigorous proofs, we narrow down the types as best as possible and then use QuickCheck to see whether something typically works as the maths would demand.
不要误会我的意思，我认为对基础进行形式化也很重要，依存类型的总体语言也很不错，但这一切都缺少了Haskell的潜力所在.至少不是我针对Haskell开发的目标，包括 constrained-categories .如果有人更喜欢纯数学，我很高兴听到这一消息.
Don't get me wrong, I think formalising the foundations is important too and dependently-typed total languages are great, but all that is somewhat missing the point of where Haskell's potential really lies. At least it's not where I aim my Haskell development, including constrained-categories. If somebody who's deeper into the pure maths wants to chime in, I'm delighted to hear about it.
这篇关于为什么在Haskell中仅将本地小的笛卡尔封闭类用于Curry类是公平的?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！