Boolean blindness

-> The boolean discards it; you must later \"remember\" what it meant.

• Elaboration

  • Constructive types preserve the witness; booleans erase it.

  • When you compute isZero n, you learn one bit.

  • But you had richer information-the structure of n.

    -> The boolean discards it; you must later "remember" what it meant.

    -> As Robert Harper puts it: to use a boolean you must know its provenance, but you've blinded yourself by reducing information to a bit.

• Example

  • Boolean approach (blind)

    txt

            f = if isZero n then y else f (pred n)

    -> Information is collapsed to a bit, branched, then had to recover what you lost - pred must re-check that n is non-zero.

  • Constructive approach (witnessing)

    txt

            f = case n of
              Zero   -> y
              Succ m -> f m

    The pattern match is the proof of non-zero-ness. The witness m is the predecessor-extracted, not recomputed.