[Haskell-cafe] Current state of type-level natural number programming

[Dan Dart]

Hey!

I had a go at this too the other week and came across the same >= ==
problem you're having.

I'm not sure if it's doable this way without dependent types, but
maybe typed unary would work. I found a good video series to study by
Richard A. Eisenberg. He mentions typed unary numbers and goes over
existentials such that he doesn't have the same problem.

https://www.youtube.com/watch?v=PHS3Q-tRjFQ
https://www.youtube.com/watch?v=WHeBxSBY0fc
https://www.youtube.com/watch?v=dK5be4cdQdE
https://www.youtube.com/watch?v=8AKtqFY1ueM
https://www.youtube.com/watch?v=jPZciAJ0oaw
https://www.youtube.com/watch?v=S5Oz_w9HDs0

Hope that helps

Dan Dart