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@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. 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