safe maps within GHC?

Norman Ramsey nr at
Tue Mar 22 18:10:01 UTC 2022

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?



More information about the ghc-devs mailing list