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

Try the `elimBool` of the paper. #25

Closed xieyuheng closed 4 years ago

xieyuheng commented 4 years ago

Can you try the elimBool of the paper in your implementation ? I can not check it in my implementation. I doubt the type check algorithm has a bug.

ice1000 commented 4 years ago

Does not check for me as well: image

I'm investigating.

ice1000 commented 4 years ago

I've found the problem. It's because when I'm generating a Val to instantiate the pi type's closure: https://github.com/owo-lang/minitt-rs/blob/2dcae72b915ce46dbaaa5c017de5d9b368c7e059/src/check/expr.rs#L247 When generating an instance of One, we're still "generating" a variable (instead of using the only possible instance Unit).

Same problem also occurs in: https://github.com/owo-lang/minitt-rs/blob/2dcae72b915ce46dbaaa5c017de5d9b368c7e059/src/check/expr.rs#L103 https://github.com/owo-lang/minitt-rs/blob/2dcae72b915ce46dbaaa5c017de5d9b368c7e059/src/check/expr.rs#L113

ice1000 commented 4 years ago

It checks in my implementation now: https://github.com/owo-lang/minitt-rs/blob/f35f6b68c9cc3c62e09f0abe60c7a8dc1b698092/samples/sum-split/bool.minitt#L21-L31

xieyuheng commented 4 years ago

Your fix is smart!

  1. But why it is enough to only do it for Unit ?
  2. Is it also right (or sound) to use unification to compare readbacked norm exps?
ice1000 commented 4 years ago

But why it is enough to only do it for Unit ?

'cus in Mini-TT your Sum { True | False } are desugared to Sum { True 1 | False 1 }, note the 1.

ice1000 commented 4 years ago

Is it also right (or sound) to use unification to compare readbacked norm exps?

It is, but not necessary. Theoretically, we're supposed to eject beta-normal eta-long normal forms. By eta-long I mean terms like (\ x -> x) : Record { label: Ty } -> Record { label: Ty } are translated to (\ { label } -> { label }), in case the record is empty it becomes \ {} -> {}. The readback function in Mini-TT is not aware of the eta-long property.