[Haskell-cafe] Easy type-level math

[Станислав Черничкин]

Thanks, that looks promising. I've also discovered some tricks:
1. With TypeFamilies and PartialTypeSignatures one can write: test :: _ =>
FixedGetter i j (Int32, Int32, Int32, Int32) where test's body is:
int32Host >>>= \a -> int32Host >>>= \b -> int32Host >>>= \c -> int32Host
>>>= \d -> ireturn (a, b, c, d). Haskell will infer that "_" (skipped type
context with some type-level math on i and j) is a (KnownNat i), ((KnownNat
(i + 4)), (KnownNat (i + 4) + 4) and so on freeing the programmer from
declaring all of this manually.
2. One can specify types explicitly. For example test :: FixedGetter 0 16
(Int32, Int32, Int32, Int32) works, unexpectedly.

2016-06-21 3:12 GMT+03:00 Lana Black <lanablack at amok.cc>:

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


-- 
Sincerely, Stanislav Chernichkin.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160622/a20217e6/attachment.html>