Type universe and (possibly) universal subtyping

[ice1000]

No description provided.

[anqurvanillapy]

Is there any plans about GADT introduction?

[anqurvanillapy]

You can also use something like

data Nat : Type'0
  = zero : Nat
  | succ : Nat -> Nat;

to decouple the compound syntax of split and Sum.

[ice1000]

Is there any plans about GADT introduction?

Not for minitt-rs, but probably for OwO (and it's gonna be hard to be compatible with first-class sums)

[ice1000]

As you can see here, the sum type is already first-class. I'm trying to build a subtyping rule from it and there's already something working, like

const bool = Sum { True | False };
let a : Sum { True } = True;

let test: bool = a;

[anqurvanillapy]

Oh damn that looks crazy... but all you're doing are exceeding Mini-TT itself right now. I think it is better to have an a-step-further/intermediate ML-like language to experiment with more features, and leave this Mini-TT untouched and compatible with its original paper?

[ice1000]

Version 0.1.8 is a vanilla Mini-TT you'd expect. I'm doing experiments in future versions.

[anqurvanillapy]

Let's tag it yooo.

[ice1000]

It's mentioned in the tut. Click https://docs.rs/minitt/0.2.4/minitt/#syntax-trees, scroll to the previous line.

[ice1000]

I'd say it's implemented, closing in favor of #20