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 apply `id` to `id` #26

Closed xieyuheng closed 4 years ago

xieyuheng commented 4 years ago

This reveals another problem with the type check algorithm in the paper.

My implementation can not check

let id_on_id: (A: type_t, A) -> A =
  id((A: type_t, A) -> A)(id)

Due to checkI can not infer type of type_t (the universe).

This can be solved by universe in universe, but the logic will be unsound.

xieyuheng commented 4 years ago

(I hope it is ok to discuss the paper in your issues, since your repo is the most popular implementation of minitt.)

ice1000 commented 4 years ago

It's solved by my type in type support, but can also be done with the lift operation in voile-rs.