I made a summary of the rules for formation of types for simple 1-position expressions, as I understand them.
Here it is in textual form:
- A symbol, say, α, is a discrete entity, represented by a unique string of characters
- A type is created from a symbol, or from another type, with the operator
[]
(column Type, downwards in the table) - In the other "direction" (upwards in the table, column Head), the head of a type is an operation of reading a label, in the form of a symbol, from an expression. Despite being "in the other direction", it is not a dual of creating a type, as creating a type returns an expression, and reading a head returns a symbol.
- So, for example: the head of
x[][]
isx[]
, the head ofx[]
isx
, etc.. On the other direction, adding[]
tox
creates a typex[]
, tox[]
creates a typex[][]
, and so on. - The head of a symbol without brackets
x
is the symbolSymbol
, common head of all symbols without brackets - The head of
Symbol
is also justSymbol
itself, so, in a way,Symbol
is the "root" symbol of the "hierarchy" - Being a "root", a type is exceptionally created from
Symbol
by also specifying its identifying string:Symbol["name"]
, which is the symbolname
.
Here is a table representation:
Expression | Head ↑ | Type ↓ |
---|---|---|
… | ||
Symbol |
Symbol |
α |
α |
Symbol |
α[] |
α[] |
α |
α[][] |
α[][] |
α[] |
α[][][] |
… |
Are these rules correct?