Is there a tool for step-by-step reduction of haskell code?

Learn
#1

I’d like it to have commands like

:subst <ident_name>  -- substitute the definition of identifier
:reduce              -- reduce lambdas in the current expresions
:case <subexpr>      -- consider the cases what (sum typed) subexpr could be

This could be used for proving laws in general (not only in simple cases, when automatic provers like ghc-proofs can do them), but I’m interesting in it not only for this use case. Sometimes it’s hard enough to figure it out, how does some function work and why it behaves so. In this case step-by-step reduction always help me. However doing it manually is sometimes very routine and error-prone.

1 Like
#2

There’s Duet which is an interpreter for a small subset of Haskell which shows all intermediate reduction steps.

I think there are a few open problems in this area:

  • For larger programs it becomes necessary to focus on a small part of the program.
  • It is difficult to show sharing.
  • GHC first compiles the program which can make it hard to connect the evaluation strategy back to the original source code.
  • GHC Haskell implements many standard functions using advanced primitives. Naively substituting functions for their definition can lead to unreadable code.

It is possible to write such a step-by-step evaluation tool that only manipulates high level source Haskell, but that means you lose details which influence running time and memory usage.

To truly understand those details you will need to dive into the intermediate representations of GHC like Core, STG, and Cmm.

3 Likes
#3

For understanding details of how time/memory usage is influenced we definetely need to dive into Core. My use case is on the high level of abstraction though. For example:

viewM (lensM getter setter) s
  ≡ viewM (\f s -> Compose $ setter s `fmapM` (getter s >>= getCompose . f)) s
  ≡ getConst <$> getCompose (
      (\f s -> Compose $ setter s `fmapM` (getter s >>= getCompose . f))
      (Compose . pure . Const) s)
  ≡ getConst <$> getCompose (
      Compose $ setter s
        `fmapM` (getter s >>= getCompose . (Compose . pure . Const))
      )
  ≡ getConst <$> getCompose (
      Compose $ traverseLike (setter s)
        =<< (getter s >>= getCompose . (Compose . pure . Const))
      )
  ≡ getConst <$> (traverseLike (setter s) =<< (getter s >>= pure . Const))
  ≡ getConst <$> ((\v -> traverseLike (setter s) (Const v)) =<< getter s)
  ≡ getConst <$> ((\v -> traverse (setter s) (Const v)) =<< getter s)
  ≡ getConst <$> ((\v -> pure (Const v)) =<< getter s)
  ≡ getConst <$> (Const <$> getter s)
  ≡ getter s

Nevertheless Duet doesn’t seems to help in this case: I mean we should use not only evaluation end definitions substitution, but also applying laws and recursive/inductive reasoning. Of course, this cannot be done automatically, but it would be much more pleasant to do this semiautomatically with correctness checking. It doesn’t seems to be impossible, though there are some difficulties I can see here: we need type inference at least for instance resolution. That’s why I’ve tried to find something ready made before reinventing the wheel

Anyway, thanks for the link to Duet. It seems very interesting

2 Likes
#4

That sounds very interesting. I too would like to have an interactive tool that allows me to apply equational reasoning to Haskell snippets. Although it sounds difficult to implement. I wonder what the simplest possible prototype would look like.

Nitpick, this would have to use some extra steps:

    getConst <$> (Const <$> getter s)
  ≡ getConst . Const <$> getter s
  ≡ id <$> getter s
  ≡ getter s
#5

I wonder what the simplest possible prototype would look like.

For now I’m thinking at least about some dumb substitutor without any type inference on the subset of haskell. It wouldn’t provide proofs in the full sense of the word anyway, but this can be improved afterwards.

Nitpick, this would have to use some extra steps

Of course, it would have. That’s just my manual work, where I was too lazy to write all steps. Maybe then we could improve the tool to make some obvious steps by itself.

Anyway, if there’s no such tool, I’ll try to make it. Not now, though. But maybe this summer. I’m glad to here you’re intersted in. If you have your ideas and want to discuss them somehow, it would be wonderful :slight_smile:

#6

I’m already thinking about implementation details. Like, I think you at least need a parser, AST, and pretty printer. Then perhaps you can implement a rewrite mechanism on the AST.

The user interface could perhaps be text-based, but that might make it difficult to specify exactly where you want to apply a rewrite.

#7

Personally, I think this requires a theorem prover. You need to be able to express and apply laws, after all.

#8

I believe that hermit aimed to provide some equational reasoning interactive tools on top of Haskell.

1 Like
#9

Oh, I think it may also be possible to adapt parts of retrie to build an interactive rewrite system. Retrie can already handle parsing, rewrite rule application, and pretty printing. The only extra things needed would be to actually write down all the possible rewrite rules that you might want to apply.

1 Like
#10

I think ghc-debug can do this.

#11

There was a bachelor thesis at OST which attempted this, but they focused on Core rather than Haskell: Haskell Substitution Stepper / substep · GitLab

#12

It seems like using Hermit is too complicated for this stuff (proving laws for lenses etc.) It is worried about how the program will be actually evaluated and so requires much more work with rewrite rules, that I’d like to have. Maybe I’m wrong, but that’s what I feel looking on examples. And there’re some problems with polymorphic types as I see from here we’re reasonning only for mapPlus1Int, not general map, but I can’t really understand what they are (and it’s crucial for me, since I want to reason about much more abstract cases about every monad etc.). I feel I’ve missed something and don’t see, how hermit could be applied to my problem. I would be glad if you clarified this a bit

#13

I am only vaguely aware of hermit’s existence and high-level description. By now you probably know more than I do about it and you are probably right that it doesn’t suit your needs. Sorry for the noise.

#14

No reason for apologize. I’m not experienced in this area, so maybe I’m wrong. I just hoped maybe you know something more about it. Anyway just knowing about it’s existence may be helpful some way. So thank you for a reference

1 Like
#15

Great idea!
Though I see some more extra things:

  • reducing lambda applications (or retry can this?)
  • reducing case applied to constructor (the same question)
  • figuring out, what are all possible cases

I’ll try to write some examples of what we want to achieve to state exactly, what we need

#16

No, you’re right. I was too optimistic. Retrie can’t do beta or eta reductions or evaluate case expressions. Those would have to be custom built-in rules.

Also, it applies the rule at every matching point. Perhaps it would be useful to add a mechanism to give the user an option where to apply a certain rule. But that also sounds difficult to implement.