Re: Imagining a Language Without Booleans

Justin Pombrio in Imagining a Language without Booleans on 2025-09-22:

Writing all of the type rules from before but using results instead of options, we have:

if (A?E) B   :  B?E
A?E else A   :  A
A?E and B?E  :  B?E
A?E or  A?F  :  A?F
not A?E      :  E?A

And writing all of the evaluation rules:

if (Ok(x))  e  ⟼  Ok(e)
if (Err(x)) e  ⟼  Err(x)
Ok(x)  else e  ⟼  x
Err(x) else e  ⟼  e
Ok(x)  and e   ⟼  e
Err(x) and e   ⟼  Err(x)
 
Ok(x) or e ⟼ Ok(x) Err(x) or e ⟼ e
 
not Ok(x)      ⟼  Err(x)
not Err(x)     ⟼  Ok(x)

This was such a fun article which does an excellent job of building up both the language of the article as well as the theoretical programming language at the same time. Something that came to mind while following along, since we're talking about a type (Maybe, and then Either in Haskell terms) that has a Monad definition [wiki], is whether and where bind would pop out. It turns out not, which is interesting.

I'm not well-versed in Haskell's many type class abstractions, so I don't know enough to try applying any of the other interesting ones (like Applicative). But I do know Monad, and can see at least that return (in the form of Ok(x) and Err(x)) is defined, as well as sequence (>>) (in the form of and) which is the operator that acts like a "semicolon" from imperative languages. Sequence executes the left side for its "effect", for Either this is whether the computation results in a value or an error, and ignores the left-side value to return whatever is on the right side. If we tried to build bind into this language it would involve some kind of let or lambda syntax in order to provide the value x to the right-side expression, something like:

Ok(x)  bind(x) in e   ⟼  e
Err(x) bind(x) in e   ⟼  Err(x)