search

owo-lang / minitt-rs

Dependently-typed lambda calculus, Mini-TT, extended and implemented in Rust
Apache License 2.0
113 stars 3 forks source link

Type universe and (possibly) universal subtyping #7

Closed ice1000 closed 4 years ago

anqurvanillapy commented 5 years ago

Is there any plans about GADT introduction?

anqurvanillapy commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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

anqurvanillapy commented 5 years ago

Let's tag it yooo.

ice1000 commented 5 years ago

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

ice1000 commented 4 years ago

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