Zero Multiplicities for Linear Haskell

[Simon Peyton Jones]

Joseph

Great!

At the moment we have one undisputed King of Linear Haskell, and that is
Arnaud Spiwak (cc'd).  He's the person to talk to.

Everyone: it would great to broaden the base.  Relying only on Arnaud puts
him under pressure; it'd be great to have more champions for Linear Haskell
and its implementation in GHC.

Simon

On Thu, 1 Aug 2024 at 22: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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20240802/c4244de3/attachment.html>