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

Thu Jan 12 18:05:29 UTC 2023

```Hi,

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

Just a shameless plug: I deviced ghc-typelits-presburger exactly to solve such problems, and applying in conjunction with ghc-typelits-natnormalise in production code:

Formally, this augments GHC's type checker with Presburger Arithmetic Solver.

https://en.wikipedia.org/wiki/Presburger_arithmetic￼

In other words, the plugin can solve propositions in natural number arithmetic which incorporates only addition, subtraction, inequalities and constant-factor multiplication. This fragment of Peano arithmetic is known to be decidable (note that it cannot solve the proposition incorporating arbitrary (indefinite) multiplications to avoid incompleteness hell).

Although there indeed be some propositions that this plugin cannot solve, but together with ghc-typelits-natnormalise and ghc-typelits-knownnat, relatively wide range of propositions can be solved automatically in my experiences.

Thanks,

-- Hiromi ISHII
konn.jinro at gmail.com

> 2023/01/11 23:55、Henning Thielemann <lemming at henning-thielemann.de>のメール:
>
>
> 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 reasoning?
>
> 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"
>
> https://github.com/clash-lang/ghc-typelits-natnormalise/issues/33
>
>
> "Could not deduce: (n0 + 1) ~ m from the context: 1 <= m"
>
> https://github.com/clash-lang/ghc-typelits-natnormalise/issues/59
>
>
>
> So, what is the current state of the art? What libraries, what GHC extensions? Any tutorials?
> _______________________________________________
> To (un)subscribe, modify options or view archives go to:
> Only members subscribed via the mailman list are allowed to post.

-------------- next part --------------
An HTML attachment was scrubbed...
-------------- next part --------------
A non-text attachment was scrubbed...
Name: favicon.png
Type: image/png
Size: 2792 bytes
Desc: not available
-------------- next part --------------
A non-text attachment was scrubbed...
Name: wikipedia.png
Type: image/png
Size: 1313 bytes
Desc: not available