safe maps within GHC?

newer
question about mapSuccessors in...

Norman Ramsey

22 Mar 2022 22 Mar '22

2:10 p.m.

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

Show replies by date

Richard Eisenberg

25 Mar 25 Mar

3:20 p.m.

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 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-proofsfunction... _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Simon Peyton Jones

26 Mar 26 Mar

4:07 p.m.

My instinct is the same as Richard's. I had a quick look at the paper and didn't immediately grok how to use it for finite maps. Still, in the TTG work we are slowly adding more static checking to GHC's code, and the O/C stuff in Hoopl is another example. And perhaps you may find a sweet spot? Feel free to have a try, so we can evaluate whether the cost (in understanding what's going on) is worth the benefit. Simon On Fri, 25 Mar 2022 at 19:26, Richard Eisenberg 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 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-proofsfunction... _______________________________________________ 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

Norman Ramsey

28 Mar 28 Mar

1:29 p.m.

...

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 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 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-proofsfunction... _______________________________________________ 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

1149

Age (days ago)

1155

Last active (days ago)

List overview

Download

3 comments

3 participants

participants (3)

Norman Ramsey
Richard Eisenberg
Simon Peyton Jones