Timeline for What types can be written in Kind but not Lean?
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 9, 2023 at 11:01 | vote | accept | user32157 | ||
| Jan 6, 2023 at 19:05 | answer | added | Nathan | timeline score: 1 | |
| Jan 6, 2023 at 15:28 | comment | added | user32157 |
@Nathan While I understand the motivation of that example from the blog post, I still don't know what the self notation means and so I don't really understand the solution. Is P taking the role of a motive? What is P(self) in the definition of Int?
|
|
| Jan 5, 2023 at 21:52 | comment | added | Andrej Bauer | It looks a bit related to Cedille. Also, have a look at Self Types for Dependently Typed Lambda Encodings by Aaron Stump, where the idea of self-types originates from (as far as I know). | |
| Jan 5, 2023 at 19:48 | comment | added | Nathan | Are you looking for something in particular beyond the examples given in the blog post? I think the first example of smart constructors for Ints given there is pretty nice. | |
| Jan 5, 2023 at 13:27 | comment | added | Max New | This sounds like a good question for the Kind developers. I don't know if any of them hang around here. | |
| Jan 5, 2023 at 11:24 | comment | added | user32157 | I don't know! My knowledge of this topic is basically limited to trying to read that linked blog post (and knowing some dependent type theory via Lean). Unfortunately "self-type" is hard to google and I'm not up with the literature. I'm not interested in Kind per se except that it's the only place I've seen this idea. If you can answer this question in another notation, that would be appreciated. Maybe I'm really just looking for an intro to self-types that compares it concretely to dependent types? | |
| Jan 5, 2023 at 8:44 | comment | added | Andrej Bauer | Can you point to some sort of a relatively complete description of Kind, or provide a description of its capabilities that situates it in the design space of possible type theories? Or to put it another way: is this a question about self-types or about Kind specifically? | |
| S Jan 5, 2023 at 0:56 | review | First questions | |||
| Jan 5, 2023 at 1:15 | |||||
| S Jan 5, 2023 at 0:56 | history | asked | user32157 | CC BY-SA 4.0 |