etb: entailment of BBQ under assumption OMG in the WTF system (omgwtfbbq)
The usual story (e.g. TAPL chapter 20) is that either:
  • 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.
But I think there's a sleight-of-hand in the "so" in the last sentence there. Why should those types have to be definitionally equal? It's perfectly fine for intersection type systems to have types that are "equivalent", in the sense of being mutual subtypes—like (A∧B) ≤ (B∧A) and (B∧A) ≤ (A∧B)—without waving around definitional equality and legislating that A ∧ B and B ∧ A are the same type expression. What I'm reading about recursive types seems to jump from "no explicit rolls" to "these types have the same inhabitants"—yes, sure—and then to "these are indistinguishable type expressions", which seems…anti-motivated (TAPL: "induction on type expressions…naturally no longer works").

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 bardraft, anyway, so it shouldn't matter too much if the source language is clunky in this respect.)
etb: entailment of BBQ under assumption OMG in the WTF system (omgwtfbbq)
(Datasort refinements and pattern typing. May not be comprehensible without unusual specialist background. May not be comprehensible to anyone but me at this moment. That's just how I roll.)
Go through the door marked 'Unicode' )
etb: (latin stun maths)
Coherent unrestricted intersection?

A, B sorts ("Curry types", etc.)
A∧B intersection (no refinement restriction)
X, Y types ("Church types", etc.)
e1 // e2 alleged coherent merge (cf. Elaborating…)

Judgments:

   e : A   —e has sort A
   e :: X   —e has principal type X
   A ⊑ X   —A refines X


e1 : A1      A1 ⊑ X1      e1 :: X1
e2 : A2      A2 ⊑ X2      e2 :: X2      X1 ⋈ X2
————————————————————————————
            e1 // e2 : A1 ∧ A2
            e1 // e2 : A2 ∧ A1


⊢ X1 ⋈ X2 read "X1 separate from X2", such that:

• If X ≤ Y or Y ≤ X (where "≤" = at-least-as-polymorphic-as) then ⊬ X ⋈ Y
    (corollary: ⊬ X ⋈ X)
• If X and Y have distinct head constructors then X ⋈ Y
• (X1 * X2) ⋈ (Y1 * Y2) if either X1 ⋈ Y1 or X2 ⋈ Y2
• (X1 + X2) ⋈ (Y1 + Y2) if X1 ⋈ Y1 and X2 ⋈ Y2
• (X1 → X2) ⋈ (Y1 → Y2) if X1 ⋈ Y1 and X2 ⋈ Y2


α ⊑ β ⊢ A ⊑ X
—————————————
⊢ ∀α.A ⊑ ∀β.X
etb: old trolleybus in yard in Cambridge, Mass. (71 WATERTOWN SQ)
I read this piece and mostly agree (modulo that it's about talks at "tech" conferences rather than at academic conferences): As soon as you're more or less okay at delivery and slide-making, stop; every hour you spend is an hour less to do on something more productive and/or more fun, which (unless you're some kind of ~natural born public speaker~) is just about anything.

Working on giving talks is sometimes spun as learning how to explain things, but it's a pretty terrible way of learning how to do that; it's too stressful. If you want to get better at explaining things, write more. If you want to get better at making good diagrams, put diagrams in your writing. Or talk about your research one-on-one. (I think the best way of doing that may be to collaborate with them, rather than try to invent reasons to talk to them.) Or lecture, which (for whatever reason) I find way less stressful than giving a research talk (except, to some extent, the first lecture of the course).

It's very difficult to give a good talk about bad work. In rare cases, you may be able to give an impressive, and probably gimmick-ridden, talk about bad work, which may be merciful in the short term, until people actually try to read the paper. Giving an "impressive" talk about good work is also not ideal: people may remember the gimmicks more than the content. I think the best compliment I've ever received about a talk was that it was "very clean", which is also the kind of compliment that I most treasure about my papers (whether it's about the writing or the actual research). (Having a complete stranger sit down next to me before a session and exclaim, "You gave a really good talk!" is also very gratifying, but too nonspecific.)

Profile

etb: (Default)
etb

August 2015

S M T W T F S
      1
2345678
91011121314 15
16171819202122
23242526272829
3031     

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 9th, 2026 02:48 am
Powered by Dreamwidth Studios