search

RedPRL / sml-telescopes

an abstract data type for telescopes
1 stars 1 forks source link

Efficiency of telescopes #12

Closed favonia closed 7 years ago

favonia commented 7 years ago

Currently, the bottleneck of RedPRL is the the telescope library. It needs a deque, which is implemented as a list now. There are many plausible approaches:

  1. Deques as pairs of lists: constant amortized time.
  2. Deques as four lists: constant time in the worst case. See Okasaki's thesis.
  3. Deques as finger trees: constant time even with persistency.

The issue of (1) is that, depending on how we use telescopes, the amortized analysis might not apply. (3) looks clean but needs polymorphic recursion which AFAIK will be ugly in SML.

jonsterling commented 7 years ago

@favonia At one time I had tried to do finger trees, but it was just too painful to code in SML sadly, so I would lean towards one of the other two options. Do you have any recommendations?

favonia commented 7 years ago

@jonsterling I think I need to know where and how SnocView and ConsView are used in practice.

jonsterling commented 7 years ago

@favonia My guess is that the thing is used most heavily is ConsView, as in: https://github.com/RedPRL/sml-dependent-lcf/blob/master/src/dependent_lcf/lcf.fun#L35

In general, we tend to traverse a telescope from the left (in "cons" style), but we usually append to a telescope from the right (in "snoc" style).

favonia commented 7 years ago

Hmm a queue would be much simpler. Do you think we really need both views?

favonia commented 7 years ago

@jonsterling It seems no one except the library itself uses SnocView. We can probably drop it or make it super expensive. Also I only found two usage of cons in sequent.sml. It is probably not that difficult to implement output-restricted deques either. Maybe just a pair of lists is sufficient.

jonsterling commented 7 years ago

@favonia That's a great point; somehow in the beginning, I expected that both views would be used equally often, but it seems like in practice that is not the case. I like your proposal...

favonia commented 7 years ago

@jonsterling Thanks. To decide between the amortized and worst-case analysis, is it common to share the same telescope everywhere? The worst case is that we share the telescope right before the data structure would start to adjust itself, where it will have to do the same adjustment many times.

favonia commented 7 years ago

@jonsterling on the second thought the polymorphic recursion is not so hard to deal with. I paused the working because telescopes also support lots of other operations, like splice, where I wonder if there is a better data structure.

favonia commented 7 years ago

Closed as the current implementation seems fine.