Type of < x : Type | y >

#1

What is the type of < x : Type | y > and is it the same as the type of < y | x : Type >?

I think the first is a type error, while the second is Kind. Here’s my reasoning for the second:

Γ ⊢ Type : Kind
───────────────────────
Γ ⊢ < y : Type > : Kind
─────────────────────────── (empty alternative; c = Kind)
Γ ⊢ < x | y : Type > : Kind

But for the first, we get stuck:

                   Γ ⊢ < > : Type
                   ────────────────
Γ ⊢ Type : Kind    Γ ⊢ < x > : Type
─────────────────────────────────── (stuck!)

For me, one issue here is that it’s not clear if order matters within the union alternatives for the type inference rules. I’m also not sure how to fix it.

#2

Hmm, well-spotted, this is indeed a problem in the current inference rules. An ugly solution would be to add more cases for the Kind and Sort cases, along the lines of:

Γ ⊢ T : Kind  Γ ⊢ < x : T | xs... > : Kind
────────────────────
Γ ⊢ < x : T | c | xs... > : Kind

A nicer solution would be to allow unions with mixed kinds, exactly like we do with records. I’ll illustrate why I think this is sound:
Remember that < x: T | y: U > can be seen as formally sugar for forall(a: k) -> { x: T -> a, y: U -> a } -> a. If we take T: Type, U: Kind and k = Kind for example, then both T -> a and U -> a are of type Kind, and the whole has type Kind too. More generally, if T: k1 and U: k2, we can choose k = k1 ⋁ k2 and then that function typechecks and has kind k1 ⋁ k2. Thus I propose that we can, like with records, allow mixed kinds and type a union as the join of the kinds of its variant types.

The inference rules would reduce to:

─────────────
Γ ⊢ <> : Type

Γ ⊢ < ts… > : c
───────────────────  ; x ∉ < ts… >
Γ ⊢ < x | ts… > : c

Γ ⊢ T : t₀   Γ ⊢ < ts… > : t₁   t₀ ⋁ t₁ = t₂
────────────────────────────────────────────  ; x ∉ < ts… >
Γ ⊢ < x : T | ts… > : t₂

and both < x : Type | y > and < y | x : Type > would be correctly given the type Kind.

1 Like
#3

Ok, if you think it’s a problem too then I’ve raised #904 to capture it.