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