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

[石井大海]

>> I'm a heavy user of ghc-typelits-natnormalise.
>> 
>> I can feel your pain that it sometimes isn't able to solve seemingly "simple" constraints. But not all is lost in those cases. The `constraints` package allows one to solve `Nat` constraints out of thin air, provided you go through a function to do it.
>> 
>> nLEZeroIsZeroRule :: (n <= 0) :- (n ~ 0)
>> nLEZeroIsZeroRule = Sub (unsafeCoerce (Dict :: Dict (a ~ a)))
> 
> Good to know that there are ways to add missing transformations.
> 
> Ideally there would be a way without unsafeCoerce, i.e. that I could prove a property manually using some proof steps expressed in functions.

I also developed [type-natural] package, which comes with the showcase of arithmetic lemma.
This builds on [equational-reasoning] package to make proof-writing easier.

[type-natural]: https://hackage.haskell.org/package/type-natural
[equational-reasoning]: https://hackage.haskell.org/package/equational-reasoning

-- Hiromi ISHII
konn.jinro at gmail.com



> 2023/01/13 19:02、Henning Thielemann <lemming at henning-thielemann.de>のメール:
> 
> 
> On Fri, 13 Jan 2023, rowan goemans wrote:
> 
>> I'm a heavy user of ghc-typelits-natnormalise.
>> 
>> I can feel your pain that it sometimes isn't able to solve seemingly "simple" constraints. But not all is lost in those cases. The `constraints` package allows one to solve `Nat` constraints out of thin air, provided you go through a function to do it.
>> 
>> nLEZeroIsZeroRule :: (n <= 0) :- (n ~ 0)
>> nLEZeroIsZeroRule = Sub (unsafeCoerce (Dict :: Dict (a ~ a)))
> 
> Good to know that there are ways to add missing transformations.
> 
> Ideally there would be a way without unsafeCoerce, i.e. that I could prove a property manually using some proof steps expressed in functions.
> 
> 
> Alternatively, maybe I can write missing steps in a custom type checker plugin.
> 
> 
> Has someone already tried to connect SBV to a type checker plugin?
> _______________________________________________
> 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/983b2e1b/attachment.html>
-------------- 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/983b2e1b/attachment.sig>