= \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.
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
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
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@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.