Refinement Type

Refinement type is a type constrained by a predicate expression. Enumeration types and interval types are syntax sugar of refinement types.

The standard form of a refinement type is `{Elem: Type | (Pred)*}`. This means that the type is a type whose elements are `Elem` satisfying `Pred`. The type that can be used for the refinement type is Value type only.

``````Nat = 0.. _
Odd = {N: Int | N % 2 == 1}
Char = StrWithLen 1
# StrWithLen 1 == {_: StrWithLen N | N == 1}
[Int; 3] == {_: Array Int, N | N == 3}
Array3OrMore == {A: Array _, N | N >= 3}
``````

When there are multiple preds, they can be separated by `;` or `and` or `or`. `;` and `and` mean the same thing.

The elements of `Odd` are `1, 3, 5, 7, 9, ...`. It is called a refinement type because it is a type whose elements are part of an existing type as if it were a refinement.

The `Pred` is called a (left-hand side) predicate expression. Like assignment expressions, it does not return a meaningful value, and only a pattern can be placed on the left-hand side. That is, expressions such as `X**2 - 5X + 6 == 0` cannot be used as refinement-type predicate expressions. In this respect, it differs from a right-hand-side predicate expression.

``````{X: Int | X**2 - 5X + 6 == 0} # SyntaxError: the predicate form is invalid. Only names can be on the left-hand side
``````

If you know how to solve quadratic equations, you would expect the above refinement form to be equivalent to `{2, 3}`. However, the Erg compiler has very little knowledge of algebra, so it cannot solve the predicate on the right.

Subtyping rules for refinement types

All refinement types are subtypes of the type specified in the `Type` part.

``````{I: Int | I <= 0} <: Int
``````

Otherwise, the current Erg has a subtyping type rule for integer comparisons.

``````{I: Int | I <= 5} <: {I: Int | I <= 0}
``````

Smart Cast

It's nice that you defined `Odd`, but as it is, it doesn't look like it can be used much outside of literals. To promote an odd number in a normal `Int` object to `Odd`, i.e., to downcast an `Int` to `Odd`, you need to pass the constructor of `Odd`. For refinement types, the normal constructor `.new` may panic, and there is an auxiliary constructor called `.try_new` that returns a `Result` type.

``````i = Odd.new (0..10).sample!() # i: Odd (or Panic)
``````

It can also be used as a type specification in `match`.

``````# i: 0..10
i = (0..10).sample!
match i:
o: Odd ->
log "i: Odd"
n: Nat -> # 0..10 < Nat
log "i: Nat"
``````

However, Erg cannot currently make sub-decisions such as `Even` because it was not `Odd`, etc.

Enumerated, Interval and Refinement Types

The enumerative/interval types introduced before are syntax sugar of the refinement type. `{a, b, ...}` is `{I: Typeof(a) | I == a or I == b or ... }`, and `a..b` is desugarized to `{I: Typeof(a) | I >= a and I <= b}`.

``````{1, 2} == {I: Int | I == 1 or I == 2}
1..10 == {I: Int | I >= 1 and I <= 10}
1... <10 == {I: Int | I >= 1 and I < 10}
``````

Refinement pattern

Just as `_: {X}` can be rewritten as `X` (constant pattern), `_: {X: T | Pred}` can be rewritten as `X: T | Pred`.

``````# method `.m` is defined for arrays of length 3 or greater
Array(T, N | N >= 3)
.m(&self) = ...
``````