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

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: https://hackage.haskell.org/packages/search?terms=ghc-typelits-presburger 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@gmail.com

2023/01/11 23:55、Henning Thielemann のメール:

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? _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.