# 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) = ...
``````