Add N-bit integer types like `i32` and `u8`.

[ryo33]

Data

enum Type {
    /// N-bit signed integer
    Signed { bit: u8 },
    //// N-bit unsigned integer
    Unsigned { bit: u8 },
    ...
}

Subtyping

• uA <: uB if A <= B
• iA <: iB if A <= B
• uA <: iB if A < B (0x1111_u can be casted to 0x01111_i)
• uN <: 'nat for any N
• iN <: 'int for any N

Coherence

Introducing either or both of the following rules breaks the coherence of the type system

• 🚫 uN <: iN for any N
• 🚫 iN <: uN for any N

For example: Is <'int> 0b11 -1 or 3?

Syntax

'do <'u3> 0b000;
'do <'u8> 0xff;
$ 1_u8;
$ -2_i32;
*<
  & 'u8
  & 'i32
>

Naming of u8

• Following the naming of 'int and 'nat, it seems that i8 or n8 would be nice. Like i8 is a subset of 'int, n8 is a subset of 'nat. This is not strange.
• Following that u8 means "unsigned integer", it seems that s8 (means "signed integer") and u8 would be nice.
• How about p8 (means "positive integer") and i8

But I choose u8 and i8 to minimize surprises for the programmers. Non-programmers may be surprised at u8 but u8 is rare enough for most Desk codes.

How about bits type like b8

It sounds nice, but the following subtyping rules break the coherence of the type system.

1. bN <: uN for any N
2. bN <: iN for any N

So we must throw Rule 2 or both of them away.

Rule 1 is safe and uN <: bN is also safe, so we can say uN = uN. uN is used to represent bits in many languages.

[ryo33]

This can be dependent types