时间戳

首页 > 解决方案 > Hashkell中类型声明中“=”的含义

haskell - Hashkell中类型声明中“=”的含义

问题描述

当我学习 Haskell 时，我忍不住尝试从正式的角度来理解一切。毕竟，这是我作为 Scala 程序员所寻求的理论连贯性。

在我看来确实计算得很好的一件事是在 lambda 演算的总体理论中拟合类型声明的含义，并且一切都是一个表达式。是的，有 Binding，但 Binding 也不适用于类型声明。

例子

data DataType a = Data a | Datum

问题：

  1. 这里的意义是=什么？如果它是一个函数的声明，那么在 rhs 上我们将得到一个可简化为不可约值的表达式或另一个表达式（即返回一个函数）。这不是我们上面所说的。

我的困惑

我们有一个类型函数，和DataType a数据构造函数又名值构造函数。显然，类型不等于值，一个在术语级别，另一个在类型级别。根本不是同一个空间。但是，遵循此处提供的发音可能会起作用https://wiki.haskell.org/Pronunciation。是发音的。在 DataType 中就是那些值。但这是一个延伸。因为它与函数声明的语义不同。因此我很困惑。类型级别函数等于值级别函数对我来说毫无意义。Data aDatum=is

我的问题以不同的方式重新表述，以解释我在寻找什么

所以从某种意义上说，我想了解数据声明的语义以及它在哪里适合一切是一个表达式（Haskell 理论框架）？

  1. 澄清与绑定的区别。一般来说，在谈到绑定时，我们可以说它是 Unit 类型的表达式吗？否则，它是什么，它的类型是什么，它在 lambda 演算或我们应该称之为支持 Haskell 的理论框架中的什么位置？

标签： haskell

解决方案

我认为这里最简单的答案是它=没有任何特别的含义——它只是 Haskell 设计者决定用于数据类型的语法。=函数定义中的=used 和 ADT 定义中的 used之间没有特别的关系；这两种结构都用于使用 RHS 上的某种规范在 LHS 上声明某些内容，但仅此而已。这两种结构的不同之处多于相似之处。

=碰巧的是，现代 Haskell在定义 ADT 时并不一定需要使用。和GADTSyntaxGHCIGADTs语言扩展启用“GADT 语法”，这是定义 ADT 的另一种方法。它看起来像这样：

data DataType a where
    Data :: a -> DataType a
    Datum :: DataType a

这说明使用=不一定是类型声明的强制部分：它只是众多约定中的一种。

（至于为什么=Haskell设计者选择使用约定type Synonym = Maybe Int与表示一个类型，然后在 LHS 上为其分配名称。）=

推荐阅读