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

[rowan goemans]

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

foo :: (n ~ 0) => Int
foo = 10

bar :: forall (n :: Nat). (n <= 0) => Int
bar = case nLEZeroIsZeroRule @n of { Sub Dict -> foo @n }

If you can hide your contraints behind this for users of your library it 
might not such a bad option. I don't need very many of these since 
natnormalise does by far the most work for me. This just fills the gaps.

Rowan Goemans

On 1/12/23 19:10, Henning Thielemann wrote:
>
> On Fri, 13 Jan 2023, 石井大海 wrote:
>
>> 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.
>
> This sounds promising!
>
> I know that Iavor Diatchki implemented a Presburger Arithmetic Solver 
> for GHC type checking many years ago, but when I asked last time, he 
> recommended ghc-typelits-natnormalise.
>
>> 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.
>
> It is good to know that I can combine different type checker plugins.
>
> _______________________________________________
> 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.