[Haskell-cafe] [oleg.grenrus at iki.fi: Re: Easy type-level math]

[Lana Black]

Forwarding Oleg's message to the list.

----- Forwarded message from Oleg Grenrus <oleg.grenrus at iki.fi> -----

Date: Tue, 21 Jun 2016 05:27:13 +0300
From: Oleg Grenrus <oleg.grenrus at iki.fi>
To: Lana Black <lanablack at amok.cc>
Subject: Re: [Haskell-cafe] Easy type-level math
X-Mailer: iPhone Mail (13F69)

ghc-typelits-natnormalise can dismiss equality constraints, like `n + m ~ m + n`. OP needs to conjure KnownNat dictionary though, and that plugin cannot do. You can do it unsafely and manually with `reifyNat` from `reflections`:
http://hackage.haskell.org/package/reflection-2.1.2/docs/Data-Reflection.html

- Oleg

> On 21 Jun 2016, at 03:12, Lana Black <lanablack at amok.cc> wrote:
> 
> GHC currently lacks an ability to normalize type level arithmetic equations. There is a plugin however [1] that implements this feature.  I believe that's what you are looking for. 
> 
> [1] ‎https://hackage.haskell.org/package/ghc-typelits-natnormalise
> 
> From: Станислав Черничкин
> Sent: Monday, June 20, 2016 11:37 PM
> To: haskell-cafe at haskell.org
> Subject: [Haskell-cafe] Easy type-level math
> 
> With DataKinds and TypeOperators and GHC.TypeLits and, probably, KindSignatures I have:
> 
> test :: (KnownNat i, KnownNat (i + 4)) => MyType i ((i + 4) + 4)
> 
> and it's typecheck perfectly.
> 
> But what I really want to have is:
> 
> test :: (KnownNat i) => MyType i (i +8)
> 
> and it does not typecheck.
> 
> Does not ((i + 4) + 4) == (i +8)?
> 
> Does not (KnownNat i) implies (KnownNat (i + 4))? 
> 
> Did I miss something about Haskell?
> 
> -- 
> Thanks, Stanislav Chernichkin.
> 
> _______________________________________________
> 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.

----- End forwarded message -----