A sort is a set of classified elements.

Sorts are declared between `[`

and `]`

as follows:

`[ `

`<sort-name>` ... `<sort-name>`` ]`

*[Convention]* The first letter of a sort name is capitalized, e.g. Nat, Int, String.

Plural sorts can be declared with space separation.

The following is a declaration of Sort `Node`

and Sort `Edge`

:

[ Node Edge ]

A partial order over sets of sorts can be defined. For example, consider Sorts `Nat`

and `Int`

for natural numbers and integers respectively. All elements belonging to `Nat`

also belongs to `Int`

. In this case, `Nat`

is called a subsort of `Int`

, and
`Int`

is called a supersort of `Nat`

.
A sort cannot be a subsort of itself.

A partial order over sets of sorts is declared with the keyword `<`

as follows:

`[ `

`<subsort-name>`` < `

`<supersort-name>`` ]`

Example:

[ NzInt < Int ]

Sort `NzInt`

is subsort of Sort `Int`

, where `NzInt`

stands for the set of all integers except zero. Subsorts are often used for defining partial functions. For example, multiplication `*`

should be defined for all integers, but the domain of the second argument of division `/`

should be the set of non-zero integers. Those operators can be defined as follows:

op _*_ : Int Int -> Int op _/_ : Int NzInt -> Int

Original Copyright © Takahiro Seino, all rights reserved.