equi-recursive, not unlike my face
Feb. 22nd, 2015 08:40 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
etbThe usual story (e.g. TAPL chapter 20) is that either:
I'm looking at this now because the "All Your Evaluation Order" draft currently has no rolls and unrolls in the source language, which led me to write in the draft that it's "equi-recursive", which led me to go back to TAPL to make sure I'm talking about it correctly. And now I guess I'm not, because I don't intend to wave a mace around just so I can declare that two types connected only by some isomorphism are "equal".
If I don't get this sorted, I'm just going to start rolling around: the draft's target language does have "roll", and the value of saying "ha ha bidirectional typing doesn't need any silly explicit 'rolls' in the source language" is low thanks to some other design decisions I've made, so silly explicit "rolls" are The Construction to Which No One Will Object. (I have no implementation of any of the four type systems who have walked into thisbardraft, anyway, so it shouldn't matter too much if the source language is clunky in this respect.)
- You have explicit "roll" and "unroll" term constructors (or "fold" and "unfold" if, unlike a cat, you don't enjoy rolling around on the ground) to introduce and eliminate the μ connective. This means that μα. 1 + α is definitely not the same type as [(μα.1+α) / α](1 + α) = 1 + (μα. 1+α): the type μα. 1 + α is inhabited by
roll (inj1 ())
(but not by inj1()) and 1 + (μα. 1+α) is inhabited by inj1(), but not by roll (inj1 ()). And then you call what you have "iso-recursive", because (μα. 1 + α) ≠ 1 + (μα. 1 + α), though there is an isomorphism between them. Or… - You don't have "roll" and "unroll", so you make μα. A(α) ~definitionally equal~ to A(μα. A(α)), meaning that you can't tell them apart, they're just different ways of notating exactly the same type.
I'm looking at this now because the "All Your Evaluation Order" draft currently has no rolls and unrolls in the source language, which led me to write in the draft that it's "equi-recursive", which led me to go back to TAPL to make sure I'm talking about it correctly. And now I guess I'm not, because I don't intend to wave a mace around just so I can declare that two types connected only by some isomorphism are "equal".
If I don't get this sorted, I'm just going to start rolling around: the draft's target language does have "roll", and the value of saying "ha ha bidirectional typing doesn't need any silly explicit 'rolls' in the source language" is low thanks to some other design decisions I've made, so silly explicit "rolls" are The Construction to Which No One Will Object. (I have no implementation of any of the four type systems who have walked into this
no subject
Date: 2015-02-23 11:46 am (UTC)The motivation for decreeing the type expressions to be the same is the Church-style view of types:
(a) expressions are intrinsically typed, and so
(b) it is not even grammatical to consider comparing terms of different type, meaning that
(c) if you can compare terms of apparently-different type, then they must actually be definitionally equal types.
If you are slightly heterodox (hi, Noam!) then you might relax "type equality" to "a subtype relation satisfying the refinement restriction", which means that two types in a subtype relation are actually refinements of the same base type.
Heretics like John Reynolds think it can make sense to take the intersection of any two types at all, which fully abandons the Church-style typing. So there's no longer any reason to assume that types with comparable inhabitants have even a refinement-style relationship.
Personally, I am agnostic about which view is the right one. Probably Noam is right as usual, but when I asked him about it at POPL, he gave me an answer involving Isbell duality.
no subject
Date: 2015-02-23 07:42 pm (UTC)Personally, I am agnostic about which view is the right one. Probably Noam is right as usual, but when I asked him about it at POPL, he gave me an answer involving Isbell duality.
I'm not looking for a right view; intersection types (no refinement restriction) and intersection sorts (refinement restriction) are both perfectly sensible. Plus, whether something is a refinement seems to be a matter of perspective.
What I'm looking for is something that makes sense in my context: I have intersection types in which the ~refinement~ restriction is that you can only form [V/a]A ∧ [N/a]A, that is, the by-value and by-name variants of A. (It's actually written as a quantifier Дa.A(a), which bakes the restriction into the type.) As usual for intersections of any flavour, I don't have term constructs to introduce and eliminate these.
Then I have possible suspensions:
• V►A doesn't just have stationary typing rules (same term in premise and conclusion) but actually elaborates to the same term as A;
• N►A has stationary typing rules, but N►A elaborates to a thunk.
You use the possible suspensions inside the intersections:
Дa. (a►A) → A
is both a call-by-name function [N/a]((a►A) → A) = (N►A) → A, and a call-by-value function [V/a]((a►A) → A) = (V►A) → A, which elaborates the same way as A → A.
Are V►A and N►A refinements of the same type? Not by the usual understanding of refinement: not only do they have different operational behaviour, one can be a value while the other isn't. However, they have exactly the same structure apart from the …► connectives.
Is V►A definitionally equal to A? No, and I see no reason to do that. It's true that V►A and A have the same inhabitants, but I'm intentionally not putting in subtyping (instead I have a section where I wave my hands about η-expansion). Even if I had subtyping I wouldn't be forced to make V►A ≤ A and A ≤ V►A, because subtyping need not be complete!
I think I'd like to keep "roll" implicit, but introducing a definitional equality across μ-unfoldings doesn't seem to make much sense, given that I'm not introducing one for V►A = A.
So maybe what I'm really asking is: assuming that I keep the current formulation with implicit "roll" but no definitional equality, what should I call it? "Implicit iso-recursive types"?
no subject
Date: 2015-02-24 10:27 am (UTC)Γ ⊢ e ⇐ A(μa. A(a))
————————————————————
Γ ⊢ e ⇐ μa. A(a)
Which isn't obviously algorithmic. What do you do instead?
no subject
Date: 2015-02-24 10:59 am (UTC)Now I'm starting to think that, after all, explicit "roll" may be the best choice for this paper. I have explicit Λα.e and e[A] for ∀ already: I was going to just make everything ~declarative~ and let the system guess ∀-instantiations, but if it can guess ∀-instantiations then it can guess evaluation orders inside the instances, which wrecks a (CBV-biased) property of the system: if you never write any CBN types, you don't get any CBN reductions. Explicit e[A] seems like a brighter "this isn't practical!" flag than "roll".
no subject
Date: 2015-02-24 11:59 am (UTC)I'm not looking for a right view; intersection types (no refinement restriction) and intersection sorts (refinement restriction) are both perfectly sensible. Plus, whether something is a refinement seems to be a matter of perspective.
I agree completely that refinement is just a matter of perspective. What I would argue in the case of "intersections", though, is that it useful to have a single technical word that picks out what is in common between "intersection types" and "intersection sorts". And here the usual definition of intersections with a refinement restriction will do the job, because it is actually useful to view classical intersection types as combining two refinements of the universal type $U$ of pure lambda terms.
Are V►A and N►A refinements of the same type? Not by the usual understanding of refinement: not only do they have different operational behaviour, one can be a value while the other isn't. However, they have exactly the same structure apart from the …► connectives.
So I don't know enough about your system, but my inclination would be to try to think about V►A and N►A as refinements of the same type (at least temporarily) and see where that goes. The really nice idea of Reynolds 2000 (which Paul-André and I tried to explain in terms of refinement in our POPL paper) is that sometimes it's possible to relate intrinsic and extrinsic semantics in a very clean way. In Reynolds' paper, that meant that he first gave a semantics where subtyping was elaborated into coercions, but then he showed how to factor this via another semantics where terms were interpreted as maps from an environment to the universal domain. ("Factor" here is meant in the extensional sense, that given knowledge of a typing derivation alpha for a term t, the intrinsic semantics of alpha is equivalent to the untyped semantics of t wrapped in coercions -- though in terms of efficiency these interpretations might be different.)
Is V►A definitionally equal to A? No, and I see no reason to do that. It's true that V►A and A have the same inhabitants, but I'm intentionally not putting in subtyping (instead I have a section where I wave my hands about η-expansion). Even if I had subtyping I wouldn't be forced to make V►A ≤ A and A ≤ V►A, because subtyping need not be complete!
Could you explain what is the reason you do not want to have subtyping?
So maybe what I'm really asking is: assuming that I keep the current formulation with implicit "roll" but no definitional equality, what should I call it? "Implicit iso-recursive types"?
I don't have recommendations for terminology, but I just wanted to encourage you to keep this formulation if it really works and let's you avoid writing explicit rolls and unrolls. People are getting used to the idea that equality of types is a tricky issue. As Conor wrote (https://pigworker.wordpress.com/2015/01/06/observational-type-theory-the-motivation/), Never trust a type theorist who has not changed their mind about equality.
no subject
Date: 2015-02-24 07:03 pm (UTC)Could you explain what is the reason you do not want to have subtyping?
Simplicity (and, in particular, to keep the paper from getting too long). In my ICFP 2012 paper, I had one type system with subtyping, and another type system without it, with a pass that identity coercions; the metatheory is easier when you can talk about types without constantly saying "where A is a subtype of…". I don't think having subtyping in this paper would be terribly illuminating, but it's a paper-engineering decision, not a philosophical one.