Funcons-beta : Datatypes.cbs | PRETTY | PDF

Datatypes

[
  Type   datatype-values
  Funcon datatype-value
  Funcon datatype-value-id
  Funcon datatype-value-elements
]

A datatype value consists of an identifier and a sequence of values.

‘Datatype T ::= …’ declares the type T to refer to a fresh value constructor in types, and asserts T <: datatype-values.

Each constructor funcon ‘F(_:T_1,…,_:T_n)’ of the datatype declaration generates values in T of the form datatype-value("F", V_1, ..., V_n) from V_1:T_1, …, V_n:T_n.

Note that a computation X cannot be directly included in datatype values: it is necessary to encapsulate it in abstraction(X).

‘Datatype T’, followed by declarations of constructor funcons for ‘T’, allows specification of GADTs.

Built-in Type
  datatype-values

Built-in Funcon
  datatype-value(_:identifiers, _:values*) : datatype-values

Funcon
  datatype-value-id(_:datatype-values) : =>identifiers
Rule
  datatype-value-id(datatype-value(I:identifiers, _*:values*)) ~> I

Funcon
  datatype-value-elements(_:datatype-values) : =>values*
Rule
  datatype-value-elements(datatype-value(_:identifiers, V*:values*)) ~> V*

← ↑ →