<div dir="ltr"><div>Dear Joseph,</div><div><br></div><div>My familiarity with Liquid Haskell is evidently less than what I'd like to as I don't know what you mean by a ghost proof term in this context. That being said, there are design decisions to make regarding the 0 multiplicity. The biggest one is: can we pattern-match on 0-multiplicity data? The type system is much easier if we can (also it's got pretty interesting consequences in my opinion, such as the ability to call `seq` on a linear variable). But as Rodrigo Mesquita indirectly points out in his master thesis, it's probably unsound to have a case on a 0-multiplicity expression which isn't a variable. Another obstacle is that type inference for multiplicity is heuristic, and I don't think I'm being overly prudent in saying that some of these heuristics will be broken by adding a multiplicity 0. So it's quite a bit of work to get there. It's not necessarily a good idea to block your PhD on solving this particular problem. That being said, don't hesitate to reach out to me: we can have a call and discuss the particular of your problem, and maybe find workarounds, and also discuss the design of the 0 multiplicity.</div><div><br></div><div>/Arnaud<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, 1 Aug 2024 at 23:12, Zullo, Joseph Anthony <<a href="mailto:jzullo@purdue.edu">jzullo@purdue.edu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class="msg17549363696172519">
<div lang="EN-US" style="overflow-wrap: break-word;">
<div class="m_17549363696172519WordSection1">
<p class="MsoNormal">Hello GHC developers, <u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">I am Joseph Zullo, a PhD student at Purdue University. I am newly subscribed to this mailing list and my approval for GitLab is awaiting approval: my username is jazullo. I may be interested in adding Zero as a multiplicity to Linear Haskell
as discussed in the <a href="https://github.com/ghc/ghc/blob/e258ad546d96fcfffd525f9b51d237cee467ad73/compiler/GHC/Core/Multiplicity.hs#L144" target="_blank">
source code notes</a>. My current use-case is with Liquid Haskell: I have Liquid Haskell proof terms embedded in linearly typed procedures, but the “ghost” proof terms consume terms nonlinearly even though they have no bearing on the linear style of the procedure
(a binary “?” operator is used with terms to the left and proofs to the right). I am looking for any work arounds for this issue, or for any help or interest in adding zero as a multiplicity so that proof terms can be casted as non-consuming. Let me know if
there are any proper avenues for this problem and/or proposal. I greatly appreciate any direction or assistance.
<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal">Joseph<u></u><u></u></p>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</div></blockquote></div><br clear="all"><br><span class="gmail_signature_prefix">-- </span><br><div dir="ltr" class="gmail_signature"><div dir="ltr">Arnaud Spiwack<br>Director, Research at <a href="https://moduscreate.com" rel="noopener noreferrer" target="_blank">https://moduscreate.com</a> and <a href="https://tweag.io" rel="noopener noreferrer" target="_blank">https://tweag.io</a>.</div></div>