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