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.