Add `substBind` operation like `unbound` recently did

[lambdageek]

In sweirich/replib#33, unbound added substBind :: Subst a b => Bind (Name a) b -> a -> b. We should have that, too.

[mrkgnao]

I wrote the following simple utility function for myself, might be relevant:

substInto
  :: (Fresh m, Typeable b, Alpha c, Subst b c) => Bind (Name b) c -> b -> m c
substInto orig rhs = do
  (v, body) <- unbind orig
  pure (subst v rhs body)

[marklemay]

It's not the exact type signature, but this seems to work

import Unbound.Generics.LocallyNameless.Unsafe

substBind :: (Typeable a, Alpha b, Subst a b) => Bind (Name a) b -> a -> b
substBind bndb a = let (x , b) = unsafeUnbind bndb in subst x a b

disregard, there are subtle bugs with the

[marklemay]

Does it make sense to also have a generalized version over patterns?

In my own code I have gotten some mileage out of

substsBind :: (Subst b a, Typeable b, Alpha a) => Bind [Name b] a -> [b] -> a
substsBind bndb a = let (x , b) = unsafeUnbind bndb in substs (zip x a) b

because I use a list pattern often.

[sweirich]

I'd like to use this function in my pi-forall demos next week. I've set up stack to grab it from this branch, but can you merge it into main instead?

[sweirich]

I also have a slightly more general version on my fork: https://github.com/sweirich/unbound-generics/tree/instantiate that works with list patterns. (Actually, any pattern that only has a single type of name.) It's more dynamic than I'd like but seems to work.

[lambdageek]

I'd like to use this function in my pi-forall demos next week. I've set up stack to grab it from this branch, but can you merge it into main instead?

Just merging into main is good enough, or would you need a release on Hackage, too? (I'd like to merge the tests from @marklemay 's fork before doing a release)

I'll also try to cherrypick the instantiate branch later tonight.

[sweirich]

Thanks!

I can work around merging from main (I'll use a fixed version in pi-forall's stack.yaml), but of course a new release on hackage would be better.

[lambdageek]

Done. Both instantiate and substBind have been added.

[sweirich]

Thank you! I've incorporated the changes into pi-forall.