Proper classes

In set theory, a proper class is a collection of objects that is not a set, and therefore cannot be contained by another entity.

Letlang types are proper classes.

A class is defined by:

• zero or more type parameters
• one constructor parameter
• optionally a predicate that each value must validate

The constructor parameter determines the structure of the values contained in the class.

Syntax:

<class-statement> :=
    | <class-statement-no-predicate>
    | <class-statement-with-predicate>
    ;

<class-statement-no-predicate> :=
    [ "pub" ] "class" <identifier>
    [ <class-type-parameters> ]
    "(" <class-constructor-parameter> ")"
    ";"
    ;

<class-statement-with-predicate> :=
    [ "pub" ] "class" <identifier>
    [ <class-type-parameters> ]
    "(" <class-constructor-parameter> ")"
    "{" <proposition>+ "}"
    ;

<class-type-parameters> :=
    "<" <identifier> ("," <identifier>)* ">"
    ;

<class-constructor-parameter> :=
    <identifier> ":" <type-ref>
    ;

Examples

class even(n: int) {
  n % 2 = 0;
}

class odd(n: int & !even);

class vector(v: {x: number, y: number});

class unit_vector(v: vector) {
  v.x ** 2 + v.y ** 2 = 1;  # sqrt() ot needed: 1**2 = 1
}

Generics

Using generics, the Result type can be constructed:

class ok<T>(r: (@ok, T));
class err<E>(r: (@error, E));
class result<T, E>(r: ok<T> | err<E>);

(@ok, 42) is ok<int>;               # true
(@ok, 42) is err<string>;           # false
(@ok, 42) is result<int, string>;   # true

(@error, "invalid") is ok<int>;             # false
(@error, "invalid") is err<string>;         # true
(@error, "invalid") is result<int, string>; # true