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

[Lana Black]

Forwarding Oleg's message to the list.

----- Forwarded message from Oleg Grenrus <oleg.g...@iki.fi> -----

Date: Tue, 21 Jun 2016 05:27:13 +0300
From: Oleg Grenrus <oleg.g...@iki.fi>
To: Lana Black <lana...@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 <lana...@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: haskel...@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 -----
_______________________________________________
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.