New blog post: Beyond Booleans

Stream: new members

[Dan Abramov]

Continuing my Lean series, I wrote a new post:

https://overreacted.io/beyond-booleans/

(The audience is mostly programmers like me.)

Would appreciate sharing in your circles (if you think someone might find it helpful) as well as any feedback/comments in case something is factually incorrect or misleading.

Thanks!

[Lawrence Wu (llllvvuu)]

FWIW Lean does also have a == which is notation for docs#BEq.beq which returns docs#Bool which does have values Bool.true and Bool.false

[Lawrence Wu (llllvvuu)]

One potential nit is that “Lean REPL” calls to mind https://github.com/leanprover-community/repl, whereas we would normally call live.lean-lang.org the “web editor” or “playground”

[Dan Abramov]

Thanks. Corrected to "playground". I'm severely downplaying Lean booleans to avoid confusion (with a "can do booleans" to be strict) so I figured I won't expand on them here.

[suhr]

But when you write 2 + 2 = 4 in Lean, it doesn’t “collapse” into anything.

Are you sure about that? The reason why you can prove 2 + 2 = 4 with rfl is because Lean converts it into 4 = 4.

[Dan Abramov]

Ah, wording. Fair. Lemme chew on that..

[Ruben Van de Velde]

I'm not sure that wording is quite accurate

[Dan Abramov]

Yea, I'll rephrase that it specifically doesn't collapse into a true or false. I do get into "unfolding" a little bit later but it's just too much to do during exposition. At this point, the main intuition I'm fighting with is the intuition of it being immediately computed.

[suhr]

Also, you can remove magic and write Eq.refl 4 instead of by rfl. Eq is just a type family, Haskell programmers should be familiar with them.

[Dan Abramov]

Also, you can remove magic and write Eq.refl 4 instead of by rfl. Eq is just a type family, Haskell programmers should be familiar with them.

I do that at the (very) end! But I'm the kind of person who closes an article as soon as it smells like Haskell because it's just too functional-brained for me. I can't read it.

[suhr]

Also, 2 + 2 = 4 is a pretty bad example to illustrate proof irrelevance because of Hedberg’s Theorem (decidable equality implies equality of equality proofs).

[Dan Abramov]

Ah interesting, can you briefly explain this? This is a bit further than I can understand.

[Dan Abramov]

Basically, are you saying that because it's decidable, they would be equal anyway for some other reason?

[suhr]

Yep.

[suhr]

https://mini-hott.readthedocs.io/en/latest/src/HedbergLemmas.html

[Dan Abramov]

Alas, this is outside of my competence for now. I'll keep it in mind and maybe add a note. One constraint I'm working with is that my audience has never seen a proof in their life (and also doesn't know mathematics) so I'm trying to keep it very easy to mentally parse.

[Dan Abramov]

I guess pedantically it still doesn't hurt to say that all proofs are equal (since it's still correct) but maybe remove the "proof irrelevance" title so that this particular example doesn't claim to be an example of that.

Whoever knows that this is a bad example already knows enough to not get confused by this example. And whoever doesn't know that would still walk away with the right takeaway.

[Dan Abramov]

Would it be fair to say that "proofs are opaque"? As a title of that section.

[Aaron Liu]

well that's not quite true either

[Aaron Liu]

theorems are opaque, but not every proof has to be declared using theorem

[Aaron Liu]

and you can still unfold them

[Dan Abramov]

Right. I guess I mean that you can't introspect values of a prop.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Counterpoint: I think 2 + 2 = 4 is a perfectly ok example. Hedberg's lemma just says that in certain other proof systems (such as HoTT), in which whether proofs are irrelevant depends on which proposition they are a proof of, 2 + 2 = 4 would have irrelevant proofs whereas a different proposition might not. But in Lean, all proofs are irrelevant, so any proposition works as an example.

[Aaron Liu]

Lean has definitional proof irrelevance, which is something that Hedberg's theorem doesn't give you

[Matt Diamond]

It might be cool to mention how you can simulate passing proofs around in Typescript by using opaque types

[Matt Diamond]

for example, you say "you can’t do much better than throwing a runtime error" if you want to write a function that takes a value between 0 and 1, but that's not entirely true

you could define an opaque type called BetweenOneAndZero and write a type guard that validates the input and returns the typed value

[Matt Diamond]

(Typescript doesn't yet support opaque types, so you have to simulate them, but it can still be done in a minimally hacky way)

[Matt Diamond]

something like this:

type Opaque<base, tag> = base & { __tag: tag };

type UnitInterval = Opaque<number, 'UnitInterval'>;

function isUnitInterval (input: number): input is UnitInterval {
  return 0 <= input && input <= 1;
}

function someFunction (input: UnitInterval): number {
  return input ** 2;
}

[Matt Diamond]

though this is more like a Lean Subtype than passing in a proof

[Dan Abramov]

Ah yeah that’s true. Hmm. Can you think of an example that would more strongly convey the difference? Not that I want to redo the entire section but I wonder if there’s something that type guards like this would struggle to express.

[Dan Abramov]

I guess I'd say this is still not "much" better since the actual enforcement is still done via a runtime check.

type UnitInterval = number & { __brand: 'UnitInterval' };

function makeUnitInterval(x: number): UnitInterval {
  if (x >= 0 && x <= 1) {
    return x as UnitInterval;
  }
  throw RangeError('x must be between 0 and 1');
}

function someFunction(x: UnitInterval): number {
  return x ** 2;
}

someFunction(0.5) // Doesn't typecheck
someFunction(1.2) // Doesn't typecheck
someFunction(-1) // Doesn't typecheck

someFunction(makeUnitInterval(0.5)) // Typechecks
someFunction(makeUnitInterval(1.2)) // Typechecks
someFunction(makeUnitInterval(-1)) // Typechecks

[Dan Abramov]

Alright, I made "much" a link pointing to https://gist.github.com/gaearon/966446d27de88ba4d4806a9a5b291d0a.

[Dan Abramov]

Some discussion and opportunity to answer people's questions about Lean:

https://www.reddit.com/r/typescript/comments/1mss4im/beyond_booleans/

https://www.reddit.com/r/ProgrammingLanguages/comments/1mss18c/beyond_booleans/

https://www.reddit.com/r/programming/comments/1ms7jwx/beyond_booleans/

[Matt Diamond]

yeah, I suppose the difference is that in Typescript you don't have a compile-time proof of the property... you only have a compile-time proof that you passed the value into a runtime validation function

still useful though, especially in a large codebase where it allows you to validate at the edges and preserve that information within

[Eric Wieser]

Dan Abramov said:

Right. I guess I mean that you can't introspect values of a prop.

I believe this isn't strictly the case; though I think actually doing do is very rare