Jason (jcreed) wrote,

So this morning or maybe yesterday I started trying out this idea of paring down the expressivity of HLF by compromising slightly the principle that all the extra stuff I'm adding to LF is just refinements, and instead demanding little tokens appear in the term language corresponding to world abstraction and application. Now this isn't going so far as to make these actual abstractions and applications to world abstractions, just "splats" in the usual syntactic sense, that in this case signal that an abstraction or application would have taken place. Something like:

Γ, α : world ⊢ M ⇐ A [p]
   Γ ⊢ ΛM ⇐ ∀α.A [p]

Γ ⊢ q ⇐ world     Γ ⊢ S : (A{q/α})[p] > C[r]
        Γ ⊢ (_; S) : ∀α.A [p] > C[r]

The "splat" on the introduction side of things is a unary operator Λ meant to suggest type abstraction from the 2nd-order λ-calculus, and on the elimination side, a spine element "_". This means admittedly that some external-language examples, namely the ones that require a variable to effectively have different numbers of quantifiers in different occurrences, such as

c : (o @ ∀α.∀β.ε) → (o @ ∀α.ε) → type.
- : c D D.

no longer type-check, but nothing of this sort arises in my examples. Indeed, this is perhaps closer to the way the LLF is already expressed — it marks linear application and abstraction differently. Although I made a virtue of departing from this explicitness in my proposal, I don't think it's too high a price to pay for type reconstruction actually working right.

It still seemd a little hacky to me, but I talked to Frank about it at our meeting today, and not only did he think it was acceptable, he kind of had a similar idea almost 20 years ago regarding regular ol' polymorphic type inference. That case was somewhat different, since you're really constructing real applications in place of the underscores, but he gave me some helpful pertinent advice anyhow.
Tags: hlf, work
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded