Vla*_*hev 2 logic haskell set-theory category-theory
从基础的角度来看,我希望看到Haskell中所谓的函数.
断然地看,有"事物"以关联的方式组成,具有身份功能,这在理论上就足够了.
但每个人都试图说服我,这不是函数的定义方式.函数被定义(他们说)作为一组来自两个集合(域和codoman)的元素对,满足某些条件.意味着函数只是一个集合.你无法在不是集合的东西上定义函数.
如果我们将这种方法应用于Haskell,我看到的是Hask类别只是一个子类别Sets,对我来说,看起来很奇怪.
我宁愿扩展函数的概念以适用于我们在Haskell中的内容.
这里在评论这个问题切线感动,但不是很深刻.我想听一个明确的陈述,比如"但实际上它们都是套装",或者"不,我们与集合理论无关".
有任何想法吗？注意事项？
这是一个非常复杂的话题.为了保持简单和易于管理,我们经常偷工减料并经常"撒谎".
与所有编程语言一样,Haskell有自己的语法和评估规则(操作语义).然而,仅在操作方面考虑编程语言可能是非常有限和麻烦的.当我们调用一个factorial函数时,我们不关心它是如何实现的,也不关心它提供结果所需的评估步骤的确切数量.
为了克服这种指称语义,提出了语法在一些"数学"模型中逐个解释.许多不同的程序(句法表达式)可能映射到相同的解释("语义").
据我所知,从未定义过整个Haskell语言的指称语义.但是,有一些Haskell片段的模型.这些模型通常是类别.
这里有一些例子.
如果我们(非常!)将Haskell限制为终止的,简单类型的核心,那么我们所需要的只是一个(双)笛卡尔闭合类别,并且集合的类别足以满足其产品,副产品和指数.
但是,Haskell没有终止,并且具有一般递归,因此我们需要固定点.通常这可以通过转移到完整的部分订单类别(通常是omega-CPO或DCPO之间的一个)来解决.
然后我们需要类型级别的固定点,因此我们需要考虑具有初始F-代数的类别(至少对于表现良好的函子F).这严重地使事情变得更加复杂.
我们还没有添加多态性!这尤其棘手,因为雷诺兹证明多态性不能通过集合来天真地建模("多态性不是集合理论"是主要的参考文献).所以我们现在有PER模型和相干模型(都是类别)作为一些尝试为多态提供语义.
然后我们需要类型类,GADT,更高级别,更高种类,......
实际上,我们不需要这种复杂程度.在编程时,我们通常会处理有限数量的功能,因此我们会"欺骗"自己并经常假装所有内容都像一个集合,或者足够接近.然后,如果确实需要,我们会增加复杂性
| 归档时间： |
|
| 查看次数： |
231 次 |
| 最近记录： |