Initial objects (or the empty map)

#1

I’m not at all into type theory, so this is mostly based on my intuitions from category theory and mathematics in general.

As far as I understand True === False is an unpopulated type. This reminds me of an initial object. So for each type A there should be a canonical function gA : True === False -> A (like, for example, the empty map in set theory). Is there a way to write down this function in Dhall or reference it in some way? Not that I need it for any practical reasons, I am just curious.

Dually, as far as I understand, True === True is populated by a unique element. It reminds me of a final object. We can β€œaccess” the unique element via assert : True === True. For each type A we have a canonical function fA : A -> True === True that we can write down explicitly: fA = \(x : A) -> assert : True === True.

#2

Yes, your intuition is correct. In particular, you’re right that there should in theory be a function like (True ≑ False) β†’ βˆ€(a : Type) β†’ a.

It helps if you think about how ≑ would be implemented if it weren’t built into Dhall. The usual way that people usually do this is the Leibniz equalilty which is basically:

a ≑ b = βˆ€(f : Type β†’ Type) β†’ f a β†’ f b

… or in the case where a and b are Bools then it would be:

a ≑ b = βˆ€(f : Bool β†’ Type) β†’ f a β†’ f b

Note: Notice how the argument of f changes based on which two things we’re comparing. We could define ≑ to be a poly-kinded function to work around that like this:

(a ≑ b) (k : Kind) = βˆ€(f : k β†’ Type) β†’ f a β†’ f b

… but that’s even less ergonomic. This is why ≑ is defined to be a language built-in in Dhall rather than implemented as Leibniz equality in the Prelude.

So if you plug in a = True and b = False into that you get:

True ≑ False = βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False

So then it’s a matter of choosing an appropriate f so that the right-hand side gives us forall (a : Type) β†’ a. In this case we can pick the following (dependent) type:

-- This is legal Dhall code!
f = Ξ»(b : Bool) β†’ if b then { } else βˆ€(a : Type) β†’ a

… and so if we plug in that f we get:

assert : True ≑ False

= assert : βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False

-- Therefore:
(assert : βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False)
  (Ξ»(b : Bool) β†’ if b then { } else βˆ€(a : Type) β†’ a)
    : { } β†’ βˆ€(a : Type) β†’ a

-- Therefore:
(assert : βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False)
  (Ξ»(b : Bool) β†’ if b then { } else βˆ€(a : Type) β†’ a)
  {=}
    : βˆ€(a : Type) β†’ a

… and that’s how True ≑ False is equivalent to βˆ€(a : Type) β†’ a.

So while that last example is not legal Dhall code (since we replace the type of assert with an equivalent type for Leibniz equality which the interpreter won’t accept), we can create a valid Dhall example that does work and prove the concept:

Ξ»(assert_ : βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False) β†’
  assert_ (Ξ»(b : Bool) β†’ if b then {} else βˆ€(a : Type) β†’ a) {=}

… and if we infer the type of that we get:

$ dhall --annotate --file test.dhall
  ( Ξ»(assert_ : βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False) β†’
      assert_ (Ξ»(b : Bool) β†’ if b then {} else βˆ€(a : Type) β†’ a) {=}
  )
: βˆ€(assert_ : βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False) β†’ βˆ€(a : Type) β†’ a

… and that type annotation is basically saying that the Leibniz encoding of True ≑ False can be converted to βˆ€(a : Type) β†’ a.

It’s also not hard to convert in the other direction, too:

Ξ»(absurd : βˆ€(a : Type) β†’ a) β†’
  absurd (βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False)

  (Ξ»(absurd : βˆ€(a : Type) β†’ a) β†’ absurd (βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False))
: βˆ€(absurd : βˆ€(a : Type) β†’ a) β†’ βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False

… so since we can convert back and forth between those types we can hand-wave that they’re isomorphic:

(True ≑ False) β‰… (βˆ€(a : Type) β†’ a)

Strictly speaking, we’d also have to prove that composing the two conversion functions in either order gives us the identity function. If you do the obvious thing and stick the two composition orders into Dhall:

let f =
      Ξ»(assert_ : βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False) β†’
        assert_ (Ξ»(b : Bool) β†’ if b then {} else βˆ€(a : Type) β†’ a) {=}

let g =
      Ξ»(absurd : βˆ€(a : Type) β†’ a) β†’
        absurd (βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False)

in  { forward = Ξ»(x : βˆ€(a : Type) β†’ a) β†’ f (g x)
    , backward = Ξ»(y : βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False) β†’ g (f y)
    }

… and then Ξ²-reduce that you just get this:

$ dhall --file test.dhall           
{ backward =
    Ξ»(y : βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False) β†’
      y
        (Ξ»(b : Bool) β†’ if b then {} else βˆ€(a : Type) β†’ a)
        {=}
        (βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False)
, forward =
    Ξ»(x : βˆ€(a : Type) β†’ a) β†’
      x
        (βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False)
        (Ξ»(b : Bool) β†’ if b then {} else βˆ€(a : Type) β†’ a)
        {=}
}

… the Ξ²-reduction gets stuck. I’m guessing it should be possible to prove (based on the types of x and y) that both the forward and backward fields evaluate to the identity function, but I don’t yet know how to do that.

2 Likes
#3

If you can find f and g such that forward and backward both normalize to the identity, that’s called a β€œdefinitional isomorphism” (an isomorphism with definitional equalities).

I doubt it is possible here, though, since x and y are very stuck (they are uninhabited) and I don’t think there’s a solution where they aren’t at the head of the term.

However, because they are magic falsey types, you can prove within Dhall that they propositions, meaning that backward x === x and forward x === x:

let p1
    : βˆ€(x : βˆ€(a : Type) β†’ a) β†’ βˆ€(y : βˆ€(a : Type) β†’ a) β†’ x ≑ y
    = Ξ»(x : βˆ€(a : Type) β†’ a) β†’ Ξ»(y : βˆ€(a : Type) β†’ a) β†’ x (x ≑ y)

let p2
    : βˆ€(x : βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False) β†’
      βˆ€(y : βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False) β†’
        x ≑ y
    = Ξ»(x : βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False) β†’
      Ξ»(y : βˆ€(f : Bool β†’ Type) β†’ f True β†’ f False) β†’
        x (Ξ»(b : Bool) β†’ x ≑ (if b then x else y)) (assert : x ≑ x)

in  { p1, p2 }
2 Likes
#4

Thanks a lot for the explanations and the time you took to write them down!