Zero Multiplicities for Linear Haskell

[Arnaud Spiwack]

Dear Joseph,

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.

/Arnaud

On Thu, 1 Aug 2024 at 23:12, Zullo, Joseph Anthony <jzullo at purdue.edu>
wrote:

> Hello GHC developers,
>
>
>
> 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 source code notes
> <https://github.com/ghc/ghc/blob/e258ad546d96fcfffd525f9b51d237cee467ad73/compiler/GHC/Core/Multiplicity.hs#L144>.
> 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.
>
>
>
> Joseph
>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>


-- 
Arnaud Spiwack
Director, Research at https://moduscreate.com and https://tweag.io.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20240802/443ddaea/attachment.html>