[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 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?
> _______________________________________________
> 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.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20230113/7a18be58/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: favicon.png
Type: image/png
Size: 2792 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20230113/7a18be58/attachment.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: wikipedia.png
Type: image/png
Size: 1313 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20230113/7a18be58/attachment-0001.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: Message signed with OpenPGP
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20230113/7a18be58/attachment.sig>