5 ms·
> Consider the standard definition of typelevel Peano numbers. > A function that maps positive integers to Peano numbers can be defined as follows Really? Tha
by noncoml 8y ago
> 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?
- imh 8y agoPeano numbers are kind of a classic first typelevel programming example. Maybe it's their unofficial Hello World. Booleans and natural numbers are usually the start, but natural numbers are complex enough to show the pain points.
- type_enthusiast 8y agoAs a shapeless enthusiast I agree with you that the Peano examples (which seem to be the go-to for any dependent types demo; not just for Scala... they must think it's helpful!) is terrible for people who don't already get dependent typing and logic programming. Which are the people you're supposed to be reaching with a demo. 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.
- rs86 8y agoYep, it's hard to grasp for engineers, this kind of thing requires training in formal logics to get started with. I think things will not make much sense until one gets that the type system can be a formal system equivalent to logic