Merging of unions containing types

(Philip Potter) #1

Currently, the expression

merge { T = λ(t : Type) → λ(x : t) → x } < T = Natural >

does not typecheck, either in the standard or in the Haskell implementation. dhall-haskell gives a confusing error

Error: Unbound variable: t

The standard does not allow this to typecheck because the relevant judgment:

Γ ⊢ t :⇥ { y : ∀(x : A₀) → T₀, ts… }
Γ ⊢ u :⇥ < y : A₁ | us… >
Γ ⊢ (merge { ts… } < us… > : T₁) : T₂
A₀ ≡ A₁
↑(-1, x, 0, T₀) = T₁
────────────────────────────────────  ; `x` not free in `T₀`
Γ ⊢ merge t u : T₀

has the condition "x not free in T₀". This condition disallows the function

λ(t : Type) → λ(x : t) → x

as a handler because it has type:

∀(t : Type) → ∀(x : t) → t

In this type, t is free in ∀(x : t) → t so the condition fails.

My question is: why? What is this condition for? It seems perfectly reasonable to me that

merge { T = λ(t : Type) → λ(x : t) → x } < T = Natural >

should normalize to:

λ(x : Natural) → x

Is there some weird edge case of the type system requires this condition?

(Philip Potter) #2

haha, sometimes once you write down your question, that’s what you need in order to work the answer out for yourself.

This becomes clearer when you consider unions with multiple alternatives. Imagine a union type < A : Natural | B : Text > and a handler record type { A : Natural -> Text, B : Text -> Text }. mergeing these two will necessarily create a value of type Text. This works because the RHS of all the handler functions is the same, so each handler will output a value of type Text.

But if the RHS of a handler function is allowed to depend on the LHS, as in ∀(t : Type) → ∀(x : t) → t, then the type of the output of each handler isn’t guaranteed to be the same. So it’s no longer clear what the type of merge t u would be.

I don’t know if I’ve explained myself very well here, but I at least think I’ve answered my own question in a way that I understand. :slight_smile:

(Gabriel Gonzalez) #3

@philandstuff: Yeah, you’ve got it right.

The way I think about it is to think in terms of the equivalent encoding using System F. A union type of the form:

< Alternative0 : Type0 | Alternative1 : Type1 >

… is equivalent to the following System F type:

  ∀(Result : Type)
→ ∀(Alternative0 : Type0 → Result)
→ ∀(Alternative1 : Type1 → Result)
→ Result

In other words, it’s encoded as a “pre-formed” merge where if you supply the expected result type and a handler for each alternative then it produces the desired result.

As you noted, if the Result type depends on a handler-specific bound variable, then there’s no Result type you can choose that will permit both handlers to type-check.