Timeline for Typing inference as a map on abstract syntax trees
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 17, 2021 at 16:50 | comment | added | xrq | Sounds a bit like Garrigue and Remy's ambivalent types (?) for GADTs. Doesn't really sound like what you want, but there is something like "up to a graph isomorphism". Yes, the types should be represented as graphs not just trees! But then this is pretty far away from MLTT... | |
| Mar 16, 2021 at 10:43 | history | edited | user61651 | CC BY-SA 4.0 |
added 147 characters in body
|
| Mar 14, 2021 at 19:30 | comment | added | Andrej Bauer | But we do. "Up to judgemental equality" is a lot more rigid than "up to homotopy". For instance, if $t : A$ and $A \simeq B$ then it does not follow that $t : B$, you have to transport $t$ explicitly to $B$. | |
| Mar 14, 2021 at 18:19 | comment | added | user61651 | Just from a homotopy perspective we can think of terms as points of spaces and equalities as paths so I wondered if we could rigidify typing. | |
| Mar 14, 2021 at 18:12 | comment | added | Andrej Bauer | That sounds very restrictive. Why would you want that? Normally one instead has uniqueness of typing: if $\Gamma \vdash t : A$ and $\Gamma \vdash t : B$ then $\Gamma \vdash A \equiv B$. | |
| Mar 14, 2021 at 18:04 | comment | added | user61651 | @AndrejBauer the question is imprecise but I want a more unique typing where terms have a type not only unique to to judgmental equality but rather unique up to isomorphism of abstract syntax trees. I will try to make it more precise. | |
| Mar 14, 2021 at 17:20 | comment | added | Andrej Bauer | The answer to the question about normal forms is obviously negative, $\mathrm{refl}(0)$ is normal inhabitant of the non-normal type $\mathrm{Id}(\mathbb{N}, 0, (\lambda x . x) 0)$. | |
| Mar 14, 2021 at 17:18 | comment | added | Andrej Bauer | Just to be sure: you really mean type inference and not type checking? | |
| Mar 14, 2021 at 15:29 | answer | added | Jesper | timeline score: 3 | |
| Mar 14, 2021 at 6:30 | history | asked | user61651 | CC BY-SA 4.0 |