
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
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/com.... 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs