safe maps within GHC?

[Norman Ramsey]

 > Feel free to have a try, so we can evaluate whether the
 > cost (in understanding what's going on) is worth the benefit.

Sounds good.  This experiment goes on my "someday/maybe" list.


Norman


 > On Fri, 25 Mar 2022 at 19:26, Richard Eisenberg <lists at richarde.dev> wrote:
 > 
 > > I've tried once or twice to introduce more static checking in the GHC
 > > source code. My limited experience with this is that the effort is large,
 > > and the payoff small. Maybe your experience will be different -- I haven't
 > > tried the particular technique in that paper -- but I probably wouldn't
 > > personally invest much energy in this direction.
 > >
 > > Richard
 > >
 > > > On Mar 22, 2022, at 2:10 PM, Norman Ramsey <nr at cs.tufts.edu> wrote:
 > > >
 > > > A blog post of lexi-lambda's recently put me onto Matt Noonan's
 > > > technique "Ghosts of Departed Proofs" [1], which appeared in the 2018
 > > > Haskell Symposium.  One example that intrigued me was a safe `Map`,
 > > > which uses the type system to guarantee that lookup does not fail.
 > > > Maps are used pretty extensively in Cmm-land; for example, I recently
 > > > have been using them to get information like the dominator set or the
 > > > reverse postorder number of every node in a `CmmGraph`.  In these
 > > > maps, every `Label` that appears in the `CmmGraph` is expected to have
 > > > an entry.  For the moment, I am just using the standard lookup
 > > > function; if an entry should be missing, my code calls `panic`.
 > > > The idea of eliminating these calls and getting compile-time type
 > > > safety is intriguing, but I'm not sure the game is worth the candle.
 > > >
 > > > What do other GHC devs think?
 > > >
 > > >
 > > > Norman
 > > >
 > > >
 > > >
 > > >
 > > > [1]
 > > https://iohk.io/en/research/library/papers/ghosts-of-departed-proofsfunctional-pearls/
 > > > _______________________________________________
 > > > ghc-devs mailing list
 > > > ghc-devs at haskell.org
 > > > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
 > >
 > > _______________________________________________
 > > ghc-devs mailing list
 > > ghc-devs at haskell.org
 > > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
 > >
 >