<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">Hi,<div><br></div><div><blockquote type="cite">I know of ghc-typelits-natnormalise, but it has some problems with inequalities that I need:<br><br>"Could not deduce n~0 from the context n<=0"<br>"Could not deduce: (n0 + 1) ~ m from the context: 1 <= m"<br><br>So, what is the current state of the art? What libraries, what GHC extensions? Any tutorials?</blockquote></div><div><br></div><div>Just a shameless plug: I deviced ghc-typelits-presburger exactly to solve such problems, and applying in conjunction with ghc-typelits-natnormalise in production code:</div><div><br></div><div><div style="display: block;"><div style="-webkit-user-select: all; -webkit-user-drag: element; display: inline-block;" class="apple-rich-link" draggable="true" role="link" data-url="https://hackage.haskell.org/packages/search?terms=ghc-typelits-presburger"><a style="border-radius:10px;font-family:-apple-system, Helvetica, Arial, sans-serif;display:block;-webkit-user-select:none;width:300px;user-select:none;-webkit-user-modify:read-only;user-modify:read-only;overflow:hidden;text-decoration:none;" class="lp-rich-link" rel="nofollow" href="https://hackage.haskell.org/packages/search?terms=ghc-typelits-presburger" dir="ltr" role="button" draggable="false" width="300"><table style="table-layout:fixed;border-collapse:collapse;width:300px;background-color:#E5E6E9;font-family:-apple-system, Helvetica, Arial, sans-serif;" class="lp-rich-link-emailBaseTable" cellpadding="0" cellspacing="0" border="0" width="300"><tbody><tr><td vertical-align="center"><table bgcolor="#E5E6E9" cellpadding="0" cellspacing="0" width="300" style="font-family:-apple-system, Helvetica, Arial, sans-serif;table-layout:fixed;background-color:rgba(229, 230, 233, 1);" class="lp-rich-link-captionBar"><tbody><tr><td style="padding:8px 0px 8px 0px;" class="lp-rich-link-captionBar-textStackItem"><div style="max-width:100%;margin:0px 16px 0px 16px;overflow:hidden;" class="lp-rich-link-captionBar-textStack"><div style="word-wrap:break-word;font-weight:500;font-size:12px;overflow:hidden;text-overflow:ellipsis;text-align:left;" class="lp-rich-link-captionBar-textStack-topCaption-leading"><a rel="nofollow" href="https://hackage.haskell.org/packages/search?terms=ghc-typelits-presburger" style="text-decoration: none" draggable="false"><font color="#272727" style="color: rgba(0, 0, 0, 0.847059);">Browse and search packages | Hackage</font></a></div><div style="word-wrap:break-word;font-weight:400;font-size:11px;overflow:hidden;text-overflow:ellipsis;text-align:left;" class="lp-rich-link-captionBar-textStack-bottomCaption-leading"><a rel="nofollow" href="https://hackage.haskell.org/packages/search?terms=ghc-typelits-presburger" style="text-decoration: none" draggable="false"><font color="#808080" style="color: rgba(0, 0, 0, 0.498039);">hackage.haskell.org</font></a></div></div></td><td style="padding:6px 12px 6px 0px;" class="lp-rich-link-captionBar-rightIconItem" width="36"><a rel="nofollow" href="https://hackage.haskell.org/packages/search?terms=ghc-typelits-presburger" draggable="false"><img width="36" style="pointer-events:none !important;display:inline-block;width:36px;height:36px;border-radius:3px;" height="36" draggable="false" class="lp-rich-link-captionBar-rightIcon" alt="favicon.png" src="cid:C4BE94E1-A78F-4E6A-8E8A-4FC67A44FF86"></a></td></tr></tbody></table></td></tr></tbody></table></a></div></div><br></div><div><br></div><div>Formally, this augments GHC's type checker with Presburger Arithmetic Solver.</div><div><br></div><div><div style="display: block;"><div style="-webkit-user-select: all; -webkit-user-drag: element; display: inline-block;" class="apple-rich-link" draggable="true" role="link" data-url="https://en.wikipedia.org/wiki/Presburger_arithmetic"><a style="border-radius:10px;font-family:-apple-system, Helvetica, Arial, sans-serif;display:block;-webkit-user-select:none;width:300px;user-select:none;-webkit-user-modify:read-only;user-modify:read-only;overflow:hidden;text-decoration:none;" class="lp-rich-link" rel="nofollow" href="https://en.wikipedia.org/wiki/Presburger_arithmetic" dir="ltr" role="button" draggable="false" width="300"><table style="table-layout:fixed;border-collapse:collapse;width:300px;background-color:#E5E6E9;font-family:-apple-system, Helvetica, Arial, sans-serif;" class="lp-rich-link-emailBaseTable" cellpadding="0" cellspacing="0" border="0" width="300"><tbody><tr><td vertical-align="center"><table bgcolor="#E5E6E9" cellpadding="0" cellspacing="0" width="300" style="font-family:-apple-system, Helvetica, Arial, sans-serif;table-layout:fixed;background-color:rgba(229, 230, 233, 1);" class="lp-rich-link-captionBar"><tbody><tr><td style="padding:8px 0px 8px 0px;" class="lp-rich-link-captionBar-textStackItem"><div style="max-width:100%;margin:0px 16px 0px 16px;overflow:hidden;" class="lp-rich-link-captionBar-textStack"><div style="word-wrap:break-word;font-weight:500;font-size:12px;overflow:hidden;text-overflow:ellipsis;text-align:left;" class="lp-rich-link-captionBar-textStack-topCaption-leading"><a rel="nofollow" href="https://en.wikipedia.org/wiki/Presburger_arithmetic" style="text-decoration: none" draggable="false"><font color="#272727" style="color: rgba(0, 0, 0, 0.847059);">Presburger arithmetic</font></a></div><div style="word-wrap:break-word;font-weight:400;font-size:11px;overflow:hidden;text-overflow:ellipsis;text-align:left;" class="lp-rich-link-captionBar-textStack-bottomCaption-leading"><a rel="nofollow" href="https://en.wikipedia.org/wiki/Presburger_arithmetic" style="text-decoration: none" draggable="false"><font color="#808080" style="color: rgba(0, 0, 0, 0.498039);">en.wikipedia.org</font></a></div></div></td><td style="padding:6px 12px 6px 0px;" class="lp-rich-link-captionBar-rightIconItem" width="36"><a rel="nofollow" href="https://en.wikipedia.org/wiki/Presburger_arithmetic" draggable="false"><img style="pointer-events:none !important;display:inline-block;width:36px;height:36px;border-radius:3px;" width="36" height="36" draggable="false" class="lp-rich-link-captionBar-rightIcon" alt="wikipedia.png" src="cid:35605E59-01E4-4438-AFD3-4B555107B372"></a></td></tr></tbody></table></td></tr></tbody></table></a></div></div></div><div><br></div><div>In other words, the plugin can solve propositions in natural number arithmetic which incorporates only addition, subtraction, inequalities and constant-factor multiplication. This fragment of Peano arithmetic is known to be decidable (note that it cannot solve the proposition incorporating arbitrary (indefinite) multiplications to avoid incompleteness hell).</div><div><br></div><div>Although there indeed be some propositions that this plugin cannot solve, but together with ghc-typelits-natnormalise and ghc-typelits-knownnat, relatively wide range of propositions can be solved automatically in my experiences.</div><div><br></div><div>Thanks,</div><div><br><div>
-- Hiromi ISHII<br>konn.jinro@gmail.com<br><br><br>
</div>
<div><br><blockquote type="cite"><div>2023/01/11 23:55、Henning Thielemann <lemming@henning-thielemann.de>のメール:</div><br class="Apple-interchange-newline"><div><div><br>Almost ten years ago I tried to convert the package llvm-tf to use type-level naturals but it did not lead very far.<br><br>What is the current state of type-level natural number programming and reasoning?<br><br>I need type-level naturals for vectors of static size.<br>The type checker must know things like:<br><br>n+n ~ 2*n<br>n*m ~ m*n<br><br>(Pos - positive natural number)<br>n::Nat, m::Pos -> n+m :: Pos<br>n::Nat, m::Pos -> n*m :: Nat<br>n::Pos, m::Pos -> n*m :: Pos<br><br><br>I need to access an element from a heterogeneous list with a typenat index. That is, I need a kind of induction.<br><br><br>I know of ghc-typelits-natnormalise, but it has some problems with inequalities that I need:<br><br>"Could not deduce n~0 from the context n<=0"<br><br>https://github.com/clash-lang/ghc-typelits-natnormalise/issues/33<br><br><br>"Could not deduce: (n0 + 1) ~ m from the context: 1 <= m"<br><br>https://github.com/clash-lang/ghc-typelits-natnormalise/issues/59<br><br><br><br>So, what is the current state of the art? What libraries, what GHC extensions? Any tutorials?<br>_______________________________________________<br>Haskell-Cafe mailing list<br>To (un)subscribe, modify options or view archives go to:<br>http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe<br>Only members subscribed via the mailman list are allowed to post.</div></div></blockquote></div><br></div></body></html>