Indexed Types, GADTs, Existential....

Initially, I simply wanted to write a macro to match types and lift enum declaration to the type level. For example,

#[type_enum]
enum Season { Spring, Summer, Autumn, Winter }

It is expanded like

trait Season {};
struct Spring;
impl Season for Spring;
struct Summer;
impl Season for Summer;
... 

Box<dyn Season> or &dyn Season can be matched with patterns with the macro match_t.

match_t! {
    season {
        Spring => ...,
        Summer => ...,
        ...
    }
}

But I have learned a little bit Haskell, I've found it is useful to keep enums with indexed type for safety. And I also noticed that types can be implemented with traits using specified type arguments. Then I tried my best to bring GADTs to Rust with type-level enums.

• An extended syntax for enums with indexed types
• Keep phantom types and filter unused generics for better inference

For example using GADTs:

type_enum! {
    enum Arith<T> {
        Num(i32) : Arith<i32>,
        Bool(bool) : Arith<bool>,
        Add(ArithRef<i32>, ArithRef<i32>) : Arith<i32>,
        Or(ArithRef<bool>, ArithRef<bool>) : Arith<bool>,
    }
}
type ArithRef<T> = Box<dyn Arith<T>>;

We use i32 and bool as indices to distinguish different Arith, keeping type safety between numbers and booleans.

Then, I found simply match_t could also be extended. Arith<i32> is implemented for Num<i32> where T = i32. So actually, in a tagless way, we can arrange match arms to each implementation with specified type arguments of the trait. Then it can roughly simulate existential indexed types.

type_enum! {
    enum Arith<T> { /* Same as above */ }

    fn eval(&self) -> T {
        Num(i) => *i,
        Bool(b) => *b,
        Add(lhs, rhs) => lhs.eval() + rhs.eval(),
        Or(lhs, rhs) => lhs.eval() || rhs.eval(),
    }
}

On expension, return type T is specified into i32 and bool where each arm can be fit in the implementation. It makes the method extension easier for traits and introduces an existential-like semantic.

However, it could be burdensome for some well-known examples with indexed types like Vector n a. It is a compile-time safe vector with n as a natural number that represents length. Its declaration is no problem with this crate. But things like append need a large amount of thinking due to the limitation of inference in Rust...

Codes are published.
enum-typer
More Examples

1 post - 1 participant

Read full topic