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

[Henning Thielemann]

On Thu, 12 Jan 2023, Dan Dart wrote:

> 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.

So far I am using type-level decimal numbers of the 'tfp' package. My 
numbers can become a bit bigger, like 256 or 512, so Unary might be too 
slow.