can’t partially-apply built-in merge function

[dhall-lang]

can’t partially-apply built-in merge function

[Gabriella439]

@sjakobi: According to the Curry-Howard correspondence between types and propositions, an uninhabited type corresponds to a false proposition.

If we take that correspondence further the Principle of Explosion says that if you assume a false proposition then you can prove any other proposition, and the type theory analog of the Principle of Explosion is that you should be able to convert an uninhabited type to any other type.

And languages do indeed provide such support for converting empty sum types to any type! For example, in Agda this is known as an "absurd pattern match", which looks like this:

https://github.com/agda/agda-stdlib/blob/cfbeba9f006418a4ceee5ad8628da5e296532a96/README/Case.agda#L26-L29

Haskell has the same feature, too, in the form of the EmptyCase language extension:

https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#extension-EmptyCase

To make this more concrete, both ∀(a : Type) → a and <> are uninhabited types in Dhall, meaning that we cannot create a value that has those types. Since they are uninhabited types then by the Principle of Explosion we should be able to convert those types to any other type (and we can!)

For example, we can convert a value of type ∀(a : Type) → a to any other type (like Integer) by just instantiating it to the desired type. For example:

λ(impossible : ∀(a : Type) → a) → impossible Integer

We can do the same thing for <>, by doing an "empty pattern match" on it, which is equivalent to absurd, as you noted:

λ(impossible : <>) → merge {} impossible : Integer

So you might wonder: are these two uninhabited values the "same" uninhabited value or two separate uninhabited values? The answer (in category theory terms) is that they are "essentially" the same if we can reversibly convert back and forth between them, and we can!

let forward : <> → (∀(a : Type) → a)
      = λ(x : <>) → λ(a : Type) → merge {=} x : a

let backward : (∀(a : Type) → a) → <>
      = λ(y : ∀(a : Type) → a) → y <>

in  {=}

If we can reversibly convert between these two types then they are "isomorphic" and the two conversion functions between them (e.g. forward and backward) are "isomorphisms". You can think of "isomorphic" as another way of saying "equivalent".

You'll recognize one of those two functions, which is the absurd function you just asked about. absurd is one of the two isomorphisms between <> and ∀(a : Type) → a.

You might also wonder: is it possible to have two uninhabited types in the language that are not isomorphic? The answer is: no! Or in other words, there can only be one uninhabited type if you treat isomorphic uninhabited types as being the same type.

To see why, we first need to answer another question: How do we prove that a type is uninhabited?

The standard way to prove that a type T is uninhabited is to create a value of type T → ∀(a : Type) → a. In fact, many languages that are used as proof assistants even define a Not type-level function for this purpose (which we can also do in dhall):

let Not : Type → Type
      = λ(T : Type) → (T → ∀(a : Type) → a)

-- This is a proof that `∀(a : Type) → a` is uninhabited
let example0 : Not (∀(a : Type) → a)
      = λ(x : ∀(a : Type) → a) → x

-- This a proof that `<>` is uninhabited
let example1 : Not <>
      = λ(x : <>) → λ(a : Type) → merge {=} x : a

in  {=}

However, if we remove language support for an "empty merge" then we have no way to prove that <> is uninhabited.

More generally, if we define "uninhabited" to mean "convertible to ∀(a : Type) → a" then by that definition all uninhabited types must be isomorphic. Here's the proof:

• Assume that a type T is "uninhabited"
• By the above definition of "uninhabited" there exist be a value forward of type Not T
• forward : Not T is the same as forward : T → ∀(a : Type) → a
• We also know that there exists a function backward of type (∀(a : Type) → a) → T
  • Proof: the implementation of backward is: λ(impossible : ∀(a : Type) → a) → impossible T
• forward and backward are isomorphisms ,therefore T is isomorphic to ∀(a : Type) → a

Therefore, all uninhabited types are isomorphic to ∀(a : Type) → a and therefore transitively isomorphic to each other.

TL;DR: Without absurd : <> → ∀(a : Type) → a we can't prove that <> is uninhabited

[Gabriella439]

@sellout: I think if we had to provide a type annotation then it would defeat the purpose since it would be more verbose than the equivalent lambda. With the type annotation you have to specify the Output type:

merge { ... } : Input → Output

... whereas with the lambda you only have to specify the Input type:

λ(x : Input) → merge { ... } x

[Gabriella439]

@nbouscal: So I can't yet figure out how to fix the reference to the following line, but I can improve the error message. See: dhall-lang/dhall-haskell#1015

[Gabriella439]

Yeah, this is definitely fixable and I've wanted this myself on a few occasions but never got around to fixing the semantics to permit it. Give me a few days and I'll propose a change to the standard to permit this

[Gabriella439]

So I was looking at this more closely and now I remember that the main reason why it's still this way is to easily support the case of type-checking a merge on an empty union type, like:

λ(x : <>) → merge x {=} : Bool

It is possible to still implement this but it would entail similarly invasive changes to type-checking other constructs (like Optional values or empty Lists) for consistency. For now I'll probably leave it the way it is unless more people request this feature

[sellout]

I was thinking that we could either adopt the typing change from dhall-lang/dhall-haskell#622:

merge Bool {=}

or the required annotation would look like

merge {=} : <> → Bool

which isn’t very different from the [] : List Bool case.

[Gabriella439]

Just commenting here to note that I now support partially applying merge as I commented in dhall-lang/dhall-haskell#622 (comment). Summarizing that comment here, I think we can easily infer the type of merge when it has a non-empty record of handlers, and when it's an empty record of handlers we can still require the fully-expanded form:

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

[sellout]

I think that after #438, this is more complicated to implement.

1. There are now cases other than merge { } that need type annotations and
2. we can’t just use the first case in the record to infer the result type of the merge.

For point 1, the type of merge { A = λ(x : Bool) → if x then 1 else 0 } can be either

• < A > → Bool → Natural or
• < A : Bool > → Natural.
  and this generalizes to an arbitrary number of fields in the record, so long as they all have the same type.

For point 2, before #438, the merge function type was implied by the first case – it had to have a type A → B, and we could error if we found a case with a mismatched B. Now, A might be part of the result type (for an empty alternative), or it could be the alternative type. We can’t tell until we find a case that has type B (for an empty alternative), C → B (meaning neither alternative is empty), or C → A → B (meaning the previous alternative was empty). And if none of those happens, we need a type annotation.

Previously, I had specced/implemented merge as a function (Merge { record :: Expr, typ :: Maybe Expr }), with the merge { } case requiring a <> → A annotation. But because of point 1, I think that might be a bit too common, so perhaps a Merge { record :: Expr, union :: Maybe Expr, typ :: Maybe Expr } is a better case – it’s still partially-applicable like a function, but in cases like point 1, you can either fully-apply it or add the type annotation (or both). If it were a function, I /think/ it’d need to look like

(merge { A = λ(x : Bool) → if x then 1 else 0 } : < A : Bool > → Natural) myUnion

whereas keeping it fully built-in, but with Maybe Union that could be

merge { A = λ(x : Bool) → if x then 1 else 0 } myUnion

just as it is now.

[nbouscal]

I think adding an explicit error message about what's happening would be about equivalently useful to actually supporting partially-applied merge. Getting expecting '.', label, or whitespace and a reference to the following line is not very friendly, and while I was able to figure out what was going on fairly quickly, someone with less Haskell experience would probably have a harder time. I don't know anything about Dhall's error-handling, so I don't know whether or not it's easier than just supporting partial application, but thought it was worth mentioning as an alternative solution.

[sellout]

@sellout: I think if we had to provide a type annotation then it would defeat the purpose since it would be more verbose than the equivalent lambda.

Yeah, I agree – that’s what I was getting at in my comment – #438 makes it impractical to simply turn merge {…} into a function.

But using Merge { record :: Expr, union :: Maybe Expr, typ :: Maybe Expr } can make it work like a function in many cases, while allowing you to “fully apply” it in ambiguous[†] cases without requiring a type annotation (the typ field is still required for the λ(x : <>) → merge {=} x : Natural case).

[†]: Ambiguous merge cases used to be only merge {=} (empty union), but since #438 any union where all the alternatives have the same type is ambiguous.

[sjakobi]

So I was looking at this more closely and now I remember that the main reason why it's still this way is to easily support the case of type-checking a merge on an empty union type, like:

λ(x : <>) → merge x {=} : Bool

That's like absurd :: Void -> a, right? What is it useful for in Dhall?

the type of merge { A = λ(x : Bool) → if x then 1 else 0 } can be either

• < A > → Bool → Natural or
• < A : Bool > → Natural.
  and this generalizes to an arbitrary number of fields in the record, so long as they all have the same type.

Thanks for pointing that out! I hadn't been aware of this ambiguity.

[Nadrieril]

Given the previous discussion, in particular this point:

For point 1, the type of merge { A = λ(x : Bool) → if x then 1 else 0 } can be either

* `< A > → Bool → Natural` or

* `< A : Bool > → Natural`.
  and this generalizes to an arbitrary number of fields in the record, so long as they all have the same type.

is this issue still possible or may we close it ?

[Gabriella439]

@Nadrieril: I believe partially applied merge is no longer possible due to that constraint, so I'll go ahead and close this issue