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

Henning Thielemann lemming at henning-thielemann.de
Wed Jan 11 14:55:15 UTC 2023

Almost ten years ago I tried to convert the package llvm-tf to use 
type-level naturals but it did not lead very far.

What is the current state of type-level natural number programming and 

I need type-level naturals for vectors of static size.
The type checker must know things like:

n+n ~ 2*n
n*m ~ m*n

(Pos - positive natural number)
n::Nat, m::Pos -> n+m :: Pos
n::Nat, m::Pos -> n*m :: Nat
n::Pos, m::Pos -> n*m :: Pos

I need to access an element from a heterogeneous list with a typenat 
index. That is, I need a kind of induction.

I know of ghc-typelits-natnormalise, but it has some problems with 
inequalities that I need:

"Could not deduce n~0 from the context n<=0"


"Could not deduce: (n0 + 1) ~ m from the context: 1 <= m"


So, what is the current state of the art? What libraries, what GHC 
extensions? Any tutorials?

More information about the Haskell-Cafe mailing list