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