Timeline for What is the intuitive meaning of star and box in a pure type system?
Current License: CC BY-SA 2.5
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 30, 2010 at 14:23 | history | edited | Mike Shulman | CC BY-SA 2.5 |
fixed \Box to \square
|
| Apr 30, 2010 at 11:24 | vote | accept | Matthew | ||
| Apr 30, 2010 at 2:18 | comment | added | Jacques Carette | Yes, T is some kind of program of type *, but usually the type language is not Turing-complete, so the type-level programs are not so complicated. That's not true when you have dependent types, like some of the systems in the lambda cube. | |
| Apr 30, 2010 at 2:10 | comment | added | Matthew | Then for the "Programs" interpretation we have: t is a program of type T classified by * classified by square. I was hoping that the relationships would stay the same within a given interpretation: if we say that t is a program of type T, then it seems that T should be some kind of program of type *. Then perhaps * is the type of type-checking programs? | |
| Apr 29, 2010 at 21:40 | history | answered | Jacques Carette | CC BY-SA 2.5 |