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 <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 > -- Arnaud Spiwack Director, Research at https://moduscreate.com and https://tweag.io.
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
