Simulatenous unbound and substitute

[nomeata]

Hi,

in my application, 20% of the time is spent in unbind. In most cases where I unbind a binder, I immediately apply a substitution to it (e.g. as in beta-reduction). I (maybe naively) think that this operation should be possible without coming up with new names, simply by working on the locally nameless terms. I could imagine that this would be more efficient (and also simpler for the user, as it would not require a Fresh or LFresh constraint).

Nevertheless I could not find it. Am I missing something here?

CC’ing @spire, who has a fork of unbound.

Thanks, Joachim

[sweirich]

I don't think this function exists currently. It is very related to the "open" operation of the "Alpha" type class, but that function can only be used to replace bound names with free names.

To get your function, I think that we'll need to extend the Subst Class with an operation similar to open. It will need to keep track of the debruijn levels (like the AlphaCtx in open) but will also need to know where the variables are (using isvar in Subst).

I think we can write such a function, but no one has asked for it yet. Would you want it to work for pattern binding too? What interface should it be? Something like:

substBind :: [ Dynamic ] -> (Bind p a) -> a

(Where the list must have enough entries of the right type for the pattern. May be able to create a safer interface, but under the covers it will have to be dynamic...)

Let me think about this a little more...

[nomeata]

In my actual use case, the patterns are always single variables (λ-abstraction and β-reduction); I have actually not used the more fancier pattern bindings in my project.

^{BTW, have a look if you want to see your code in action, teaching logic and proving in a playful and (according to reddit) addictive way: http://incredible.nomeata.de/}

[sweirich]

Ok, I just pushed a new version with the function "substBind" that might work for you. (I've tested it very minimally.)

  substBind :: Subst a b => Bind (Name a) b -> a -> b

Can you try it out to see if it speeds things up in your development?

[nomeata]

I already like the type signature :-). But:

Unbound/LocallyNameless/Subst.hs:24:8:
    Could not find module ‘Unbound.DynR’
    Use -v to see a list of the files searched for.

[sweirich]

Oops. Just pushed.

[nomeata]

Hmm, the performance gains are not as large as I hoped (mostly probably insignificant), but at least I could make some of my code non-monadic this way.

BTW, you still need to list Unbound.DynR in exposed-modules or other-modules.

[nomeata]

Spoke too soon, found another spot where I could use substBind, now runtime went down by 10% in some cases, as expected. Thanks!

[sweirich]

Excellent! If you can think of other ways to make unbound faster in practice, let me know.

Another performance test you could try is to switch to https://hackage.haskell.org/package/unbound-generics. Not sure how well the interfaces match up, but the underlying generic programming structure is different, and that could have performance impact.