类型构造函数和类型常量(和类型变量):有什么区别？

Question

我对类型构造函数,类型常量和类型变量之间的区别感到困惑.

Haskell 98报告称有4种类型的表达式:

1. 输入变量
2. 键入构造函数
3. 输入申请
4. 括号类型

那么什么是类型常数？该报告称"Char,Int ...是类型常量",但我找不到更详细的例子.更令人困惑的是,如何IO首先将其称为"一元类型构造函数",然后将其称为"常量IO".

我问的原因是因为本文关于Haskell的类型系统实现.在其中,它说:

Haskell类型表达式是类型变量或常量(每个都有相关的类型),或者是一种类型到另一种类型的应用程序:将类型k1 - > k2应用于类型k1的类型生成类型k2

它说的不同于报告.第二种类型的表达式是"构造函数"还是"常量"？

该文件还包括显示代表性的代码:

data Type  = TVar Tyvar | TCon Tycon | TAp  Type Type | TGen Int
             deriving Eq

data Tyvar = Tyvar Id Kind
           deriving Eq
data Tycon = Tycon Id Kind
           deriving Eq

显然Tycon代表"型构造,"但当时是什么TCon表现？怎么样Tyvar和TVar？为什么需要分开T和Ty？

Answer 1

最后一个问题

显然Tycon代表"类型构造函数",但TCon代表什么？Tyvar和TVar怎么样？为什么需要分开T和Ty？

第一.

在"T"的TCon,TVar等仅仅是一个标志是,关注的是类型和他们类型的构造Type.TCon取一个类型的值Tycon并Type从中构造一个类型的值等.构造函数Type没有前缀,Ty而只是T为了避免混淆,类型可能已被定义

data Type = Tyvar Tyvar | Tycon Tycon | ...

因为值构造函数和类型存在于不同的名称空间中,但这会为更加混乱开辟道路.

1输入变量

是可以用其他类型表达式替换的类型表达式,它们的标识符以小写字母开头(或者它们可以是不以':'开头的符号).

2键入构造函数

是类型表达式采取零个或多个类型表达式参数来构造型种*,例如

• 诠释
• 烧焦
• 双

是nullary类型构造函数,它们采用零类型表达式参数来构造一种类型*,这些也是类型常量.

• 也许
• IO
• []

是一元类型构造函数,它们采用一种类型表达式(*在这些示例中是类型的,但是一元类型构造函数也可以采用其他类型的参数).

• 或
• (,)

是二进制类型构造函数,

• StateT

是一个三元类型的构造函数,取两种类型*和一种类型的论据* -> *(StateT因此是这种类型StateT :: * -> (* -> *) -> * -> *).

3键入应用程序

是表单的类型表达式t1 t2.如果t2有种类k2和t1有种类k2 -> k3(类似于功能应用),它只是格式良好.例如StateT s,类型应用程序,类型表达式StateT应用于类型变量s.

4括号类型

是括号中的类型表达式,可能是优先级解析或解析所必需的,否则它与未表示的类型表达式相同,例如

instance Monad (Either e) where ...

括号型表达(Either e)是相同的Either e,但括号是必需的,以从两参数类用于两个类型表达式的实例区分开来Either并e.在类型中

StateT s ((->) a) b

周围的括号(->) a是为了优先.(注意,该类型构造(->)不是由类型构造用大写字母开头的一般规则覆盖,作为一个特殊的情况下[],(,),(,,)等)

现在,输入常量.这些只是不包含类型变量的类型表达式,但我不认为它在任何地方都是正式定义的.因此,只有大写字母标识符(包括启动与符号":")的任何类型的表达式和特殊情况下([],(->),(,),...)是一种不变.

• 单个标记类型表达式以大写字母开头(符号为':')或特殊情况是类型常量
• 完全由类型常量组成的类型表达式是一个类型常量

Answer 2

在类型理论中,"类型构造函数"通常是指更高类型的类型表达式.通过扩展,普通类型通常作为退化情况包括在内.

在编程语言中,"类型构造函数"通常使用更具体的含义,指的是由上下文定义的命名类型构造函数.同样,这可以包括普通类型作为零参数的退化情况.

术语"类型常数"稍微不那么标准.在Haskell定义中,它似乎非常非正式地使用,并且可能意味着表示由语言预定义的命名类型构造函数的子集(与用户定义的类型构造函数相对,它是根据代数定义的)类型和预定义类型构造函数).因此,每个常量也是一个类型构造函数.

对于"T"vs"Ty",这似乎只是您正在查看的代码片段中的命名约定,旨在区分语言级数据构造函数("T")和语言级类型构造函数("泰").将它分解为单独的类型定义Tycon并将其Tyvar分解为单独的类型定义的原因可能是它们被某些代码单独使用.