Brandon Williams

@mbrandonw In #8, is the right way to think about this type as "Something" as in "there exists…" So does Bottom mean "there does not exist…"

@cocoaphony for example, the empty tuple `()`

@mbrandonw And I'm not clear how () applies. Can you implement Not<Void>? Is Void true?

@cocoaphony Void would be true, and it's just a typealias for the empty tuple (). Same as the empty struct `Struct {}`.

@mbrandonw If () is true, then is 1? (1,"a")? I see why Empty is convenient, but is it unique?

@cocoaphony well 1 is a value, not a type. I guess that's the confusion. The empty tuple is acting as a type and a value: let x: () = ()

@cocoaphony sorry, maybe i shouldn't have used empty tuple as an example.

@mbrandonw Curious about #2. Not just one possible answer, right? return { _ in { c, a in c } } return { g in { c, a in g(c, f(a)) } }

@uint_min huh yeah, and you can even see why in the redundancy of the propositions, which leads to multiple proofs.

@mbrandonw Very nice post. One pedantic point: each of those functions can be implemented with a call to a noreturn function like abort :-)

@mbrandonw Nice post! Takes me back to my symbolic logic course :)

@mbrandonw interesting. Minor error: P⇒Q should mean Q false if P true and Q false, true otherwise.