> Consider the standard definition of typelevel Peano numbers.
> A function that maps positive integers to Peano numbers can be defined as follows
Really? That was the simplest example you could think of?
> A function that maps positive integers to Peano numbers can be defined as follows
Really? That was the simplest example you could think of?
I have a talk to intro typelevel proofs in Scala (with shapeless as the example target), that uses the kind of geometric proofs we all did in high school as an analogy. I think that's more of an accessible metaphor, but it also seems like precisely what Odersky is trying to eliminate in Dotty - the use of inductive implicit derivation to form "proofs" of invariants that are also implementations. Admittedly, it's an approach that seems rather difficult for a lot of engineers to grasp, which means it's of questionable utility. But it always seemed really elegant to me - type systems are about proving invariants, and Scala's just gives you powerful ways to prove things by unifying that concept into implicits.