<div dir="ltr">Thanks, that looks promising. I've also discovered some tricks:<div>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 (<span style="font-size:12.8px">KnownNat i), (</span><span style="font-size:12.8px">(</span><span style="font-size:12.8px">KnownNat (i + 4)), (</span><span style="font-size:12.8px">KnownNat (i + 4) + 4) and so on freeing the programmer from declaring all of this manually.</span></div><div><span style="font-size:12.8px">2. One can specify types </span><span style="font-size:12.8px">explicitly. For example </span>test :: FixedGetter 0 16 (Int32, Int32, Int32, Int32) works, unexpectedly. </div><table class="" style="border-spacing:0px;color:rgb(119,119,119);font-size:13px"><tbody><tr><td style="padding:0px"><br></td><td colspan="2" style="padding:0px"><div class=""></div></td></tr></tbody></table><div class="gmail_extra"><div class="gmail_quote">2016-06-21 3:12 GMT+03:00 Lana Black <span dir="ltr"><<a href="mailto:lanablack@amok.cc" target="_blank">lanablack@amok.cc</a>></span>:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><div lang="en-US" style="line-height:initial;background-color:rgb(255,255,255)">                                                                                      <div style="width:100%;font-size:initial;font-family:Calibri,"Slate Pro",sans-serif,sans-serif;color:rgb(31,73,125);text-align:initial;background-color:rgb(255,255,255)">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. </div><div style="width:100%;font-size:initial;font-family:Calibri,"Slate Pro",sans-serif,sans-serif;color:rgb(31,73,125);text-align:initial;background-color:rgb(255,255,255)"><br></div><div style="width:100%;font-size:initial;font-family:Calibri,"Slate Pro",sans-serif,sans-serif;color:rgb(31,73,125);text-align:initial;background-color:rgb(255,255,255)">[1] ‎<a href="https://hackage.haskell.org/package/ghc-typelits-natnormalise" target="_blank">https://hackage.haskell.org/package/ghc-typelits-natnormalise</a></div>                                                                                                                                     <div style="width:100%;font-size:initial;font-family:Calibri,"Slate Pro",sans-serif,sans-serif;color:rgb(31,73,125);text-align:initial;background-color:rgb(255,255,255)"><br></div>                                                                                                                                                                                                   <div style="font-size:initial;font-family:Calibri,"Slate Pro",sans-serif,sans-serif;color:rgb(31,73,125);text-align:initial;background-color:rgb(255,255,255)"></div>                                                                                                                                                                                  <table width="100%" style="border-spacing:0px;background-color:white"> <tbody><tr><td colspan="2" style="font-size:initial;text-align:initial;background-color:rgb(255,255,255)">                           <div style="border-style:solid none none;border-top-color:rgb(181,196,223);border-top-width:1pt;padding:3pt 0in 0in;font-family:Tahoma,"BB Alpha Sans","Slate Pro";font-size:10pt">  <div><b>From: </b>Станислав Черничкин</div><div><b>Sent: </b>Monday, June 20, 2016 11:37 PM</div><div><b>To: </b><a href="mailto:haskell-cafe@haskell.org" target="_blank">haskell-cafe@haskell.org</a></div><div><b>Subject: </b>[Haskell-cafe] Easy type-level math</div></div></td></tr></tbody></table><div><div><div style="border-style:solid none none;border-top-color:rgb(186,188,209);border-top-width:1pt;font-size:initial;text-align:initial;background-color:rgb(255,255,255)"></div><br><div><div dir="ltr">With DataKinds and TypeOperators and GHC.TypeLits and, probably, KindSignatures I have:<div><br></div><div>test :: (KnownNat i, KnownNat (i + 4)) => MyType i ((i + 4) + 4)<br></div><div><br></div><div>and it's typecheck perfectly.</div><div><br></div><div>But what I really want to have is:</div><div><br></div><div>test :: (KnownNat i) => MyType i (i +8)</div><div><br></div><div>and it does not typecheck.</div><div><br></div><div>Does not ((i + 4) + 4) == (i +8)?</div><div><br></div><div>Does not (KnownNat i) implies (KnownNat (i + 4))? </div><div><br></div><div>Did I miss something about Haskell?</div><div><div><br></div>-- <br><div data-smartmail="gmail_signature"><div dir="ltr"><span style="font-family:arial;font-size:small">Thanks, Stanislav Chernichkin.</span><br></div></div>
</div></div>
<br></div></div></div></div>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><div data-smartmail="gmail_signature"><div dir="ltr"><span style="font-family:arial;font-size:small">Sincerely, Stanislav Chernichkin.</span><br></div></div>
</div></div>