Algorithm frameworks (TimeM, cslib#372, cslib#376)

Stream: CSLib

[Fabrizio Montesi]

@Shreyas Srinivas @Kim Morrison thanks for all the work into those PRs. I have plenty of comments, but to optimise everybody's time I'd like to understand better how TimeM, cslib#372, and cslib#376 compare. Let's focus on key points.

In a nutshell, cslib#372 gives us signatures like

def insertionSort (l : List α) : Prog (SortOpsInsertHead α) (List α)

which fights cheating through interpretation (FreeM/Prog).

By contrast, cslib#376 gives us:

public def insertionSort [Monad m] (cmp : α × α → m Bool) : List α → m (List α)

which fights cheating through parametric polymorphism.

I have two questions:

1. After squinting my eyes for a while, I could imagine ways to do almost anything interesting in both approach (reusing the same algorithm with different cost models, doing parametric complexity, proving lower bounds, etc.). Is that actually true?
2. Real bliss in this case would be using a typeclass instead of an explicit parameter for the operations, for example:

public def insertionSort [Monad m] [LE α] : List α → m (List α)

Can that be done?

[Chris Henson]

Please note cslib#275 is closed in favor of cslib#372. They are the same with squashed commit history that made it easier to review.

[Fabrizio Montesi]

That's the one I meant, thanks for spotting it. Edited.

[Shreyas Srinivas]

the point with cslib#372 is beyond just getting rid of cheating. In terms of “cheat”ability both PRs are close (and substantially better than TimeM) but as @Eric Wieser pointed out, passing explicit comparison functions can cause problems. I will let him address that issue

[Shreyas Srinivas]

The point of my Prog approach is to go far beyond what TimeM and TickM can

[Shreyas Srinivas]

To allow explicit reasoning about model and reductions between them

[Shreyas Srinivas]

And about lower bounds in some cases

[Shreyas Srinivas]

As I showed in an earlier thread we can also handle circuits (which means we can handle parallel algorithms)

[Fabrizio Montesi]

To be clear, what you're claiming is that all of that cannot be done in cslib#376?

[Shreyas Srinivas]

Yes

[Shreyas Srinivas]

And there’s more

[Shreyas Srinivas]

With an explicit query model approach we can

1. Have multiple cost models for the same query (you see examples in one of my test files)
2. You can pursue a top down and modular approach to algorithms formalization.

[Shreyas Srinivas]

To elaborate on 2. What I mean is that we follow algorithms papers and encode their opaque subroutines from Literature as queries. Then we reduce those custom queries to more basic queries, all the way down to standard models

[Shreyas Srinivas]

So we have clear reduction theorems

[Shreyas Srinivas]

I can also use this framework to make working with explicit TMs quite a bit simpler

[Shreyas Srinivas]

And since both circuits and TMs can fit into the same web of reductions, we have a chance to finally tackle uniform circuits

[Shreyas Srinivas]

slightly different issue

The generalisations of CSLib#376 could (and ideally should) be built on top of cslib#372 by converting Prog from a free monad to a free monad transformer.

[Shreyas Srinivas]

For algorithms theory I’d not use this hypothetical ProgT with any monad other than Id because adding extra monads has unexplored questions of soundness w.r.t complexity models.

[Shreyas Srinivas]

And to also be clear. None of the models above completely disallow “cheating”. They just reduce it to a point where a reviewer can easily spot it. As soon as you have a query (on in the case of cslib#376 ‘s case a function) that performs what I call a “write-operation” it can be substituted by a pure operation.

This is an inherent limitation of any monadic lightweight approach which will require human review to avoid. Both these approaches simplify this review process over TimeM. But with CSLib#372 as Eric can explain, this is simpler because of the upfront statement of queries and costs.

[Shreyas Srinivas]

And I claim that we actually want this explicit commitment for all the reasons above. In general if one cannot commit to a cost model and operations to count in advance, it is much more dangerous to do this inside an algorithm.

[Chris Henson]

An interesting aspect of 376 is its usage of mvcgen. It would be nice to make use of this, so I'd like to understand if its possible and/or what this would look like with the free monad approach.

[Shreyas Srinivas]

Yes

[Shreyas Srinivas]

I haven’t done this because my pr is big enough as it is

[Shreyas Srinivas]

But I think the basic approach of cslib#376 can be ported to cslib#372 (in a future PR)

[Shreyas Srinivas]

After all we are just evaluating in the Id monad

[Shreyas Srinivas]

And Fabrizio : I think the extra annotation’s flexibility is important.

[Shreyas Srinivas]

Today you might have an opaque query for computation Z with one cost model. Tomorrow there might be a better algorithm for Z with better time complexity. You might just want to give your existing query a new cost model for Z.

[Eric Wieser]

(note that I have some thoughts here but am away on vacation for the next week and a bit so may not find time to collect them)

[Shreyas Srinivas]

There might be two ways of building cslib#376 on top of cslib#372.

1. Eric suggested compiling these parametric monad programs to Prog for complexity.
2. I thought we could generalise Prog.eval to Prog.liftM which would lift programs to arbitrary monads while we handle complexity through Prog.time. That way we can also probably reuse the mvcgen stuff

Maybe this message goes to a different thread.