Timeline for Recursively dependent types?
Current License: CC BY-SA 2.5
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 23, 2009 at 19:39 | vote | accept | Mike Shulman | ||
| Dec 23, 2009 at 19:38 | comment | added | Mike Shulman | I don't see why that's important---I only want $z$ to have one type, namely $A(z)$. | |
| Dec 23, 2009 at 12:55 | comment | added | Neel Krishnaswami | Yeah, the same constants can participate in many types. The easiest example is with sums -- the left injection into a sum $inl(-)$ is a constant of type $A \to A + B$ for all types $A$ and $B$. | |
| Dec 22, 2009 at 23:26 | comment | added | Mike Shulman | But I think that your first couple of paragraphs give me the answer I want, because I really do want $z$ to be a constant. I had assumed that even in order for $z$ to be a declared constant of type $B$, the type $B$ would have to be a well-formed type in some context---which I guess $A(z)$ is since $z$ is a constant and all, but I had somehow felt that $B$ ought to be well-formed "before" $z$ is declared. But I guess that sort of "before" is not even applicable here. | |
| Dec 22, 2009 at 23:25 | comment | added | Mike Shulman | Thanks for the very detailed answer! I am still digesting the stuff about fixed-point operators, but I don't think it's quite relevant for what I wanted, since my indexing type $A(z)$ isn't something like $\mathbb{N}$ on which a type could be defined by recursion anyway. | |
| Dec 22, 2009 at 11:07 | history | edited | Neel Krishnaswami | CC BY-SA 2.5 |
Eliminated redundant phrasing
|
| Dec 22, 2009 at 10:08 | history | edited | Neel Krishnaswami | CC BY-SA 2.5 |
added 755 characters in body
|
| Dec 22, 2009 at 9:51 | history | answered | Neel Krishnaswami | CC BY-SA 2.5 |