function - 哪些语言是函数抽象而不是原始函数

Question

在 Haskell 中，给出了函数类型 (->)，它不是代数数据类型构造函数，并且无法将其重新实现为与 (->) 相同.

所以我想知道，什么语言可以让我编写我的 (->) 版本？这个属性怎么称呼？

UPD通过讨论重新表述问题:

哪些语言没有 -> 作为原始类型？

为什么 -> 是必要的原语？

Answer 1

我想不出有任何语言将箭头作为用户定义类型。原因是箭头——函数的类型——被嵌入到类型系统中，一直到简单类型的 lambda 演算。箭头类型必须是语言的基础，这直接来自于这样一个事实:在 lambda 演算中形成函数的方式是通过 lambda 抽象(在类型级别引入箭头)。

尽管 Marcin 恰本地指出您可以以自由点的方式进行编程，但这并不会改变您正在做的事情的本质。使用一种没有箭头类型作为原语的语言违背了 Haskell 最基本的构建 block 。 (您在问题中引用的语言。)

将箭头作为原始类型也与构造逻辑有一些重要的联系:您可以将函数箭头类型视为直觉逻辑的暗示，并将具有该类型的程序视为“证明”。 (也就是说，如果你有 A -> B 类型的东西，你就有一个证明，它采用 A 类型的一些前提，并产生 B 的证明。)

事实上，您对将箭头嵌入到语言中感到不安，这可能意味着您没有从根本上理解为什么它们与语言的设计如此紧密地联系在一起，也许是时候阅读几章了来自 Ben Pierce 的《类型和编程语言》link.

编辑:您始终可以查看没有强大函数概念的语言，并且以其他方式定义其语义(例如 forth 或 PostScript)，但在这些语言中您没有定义归纳数据类型的方式与 Haskell、ML 或 Coq 等函数式语言中的方式相同。换句话说，在任何为数据类型定义构造函数的语言中，箭头都会自然地从这些类型的构造函数中产生。但是，在不以典型方式定义归纳数据类型的语言中，您不会自然地获得箭头类型，因为该语言并不是那样工作的。

另一次编辑:我会再添加一条评论，因为我昨晚想到了这一点。函数类型(和函数抽象)构成了几乎所有编程语言的基础——至少在某种程度上，即使它是“在幕后”。但是，有些语言旨在定义其他语言的语义。虽然这与您所说的并不严格相符，PLT Redex就是这样一个系统，用于指定和调试编程语言的语义。从实践者的角度来看，它并不是非常有用(除非您的目标是设计新语言，在这种情况下它相当有用)，但也许这符合您的需求。