# Initial objects (or the empty map)

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`.

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 `Bool`s 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

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

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

Iβve raised a related issue: dhall-lang/dhall-lang/issues/1379