ekmett / bound

Combinators for manipulating locally-nameless generalized de Bruijn terms
https://www.schoolofhaskell.com/user/edwardk/bound
Other
121 stars 30 forks source link

Add predicate to substitute functions #90

Open Icelandjack opened 1 year ago

Icelandjack commented 1 year ago
substitute :: Monad f => Eq a => a -> f a -> f a -> f a
substitute = substituteOf . (==)

substituteBy :: Monad m => (a -> Bool) -> m a -> m a -> m a
substituteBy old new as = do
  a <- as
  if old a
    then new
    else pure a
substituteVar :: Functor f => Eq a => a -> a -> f a -> f a
substituteVar = substituteVarOf . (==)

substituteVarBy :: Functor f => (a -> Bool) -> a -> f a -> f a
substituteVarBy old new as = do
  a <- as
  pure
    if old a
      then new
      else a

Is there a use for this?

phadej commented 1 year ago

Isn't substitute a composition of abstract and instantiate?

--

EDIT: or alternatively is there much gained over just asking users to write as >>= \a -> ... as a general way to substitute stuff. I haven't found substituting a single variable to be a common theme (compared to performing simultaneous subsitutions) when using bound. abstract1 is common, to build up lambda like terms, but these are instantiated much later.

cartazio commented 1 year ago

Even that aside, what would it mean to not substitute a variable?

On Sat, Mar 18, 2023 at 2:17 PM Oleg Grenrus @.***> wrote:

Isn't substitute a composition of abstract and instantiate?

— Reply to this email directly, view it on GitHub https://github.com/ekmett/bound/issues/90#issuecomment-1474936985, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAABBQSBS5Y3Y3CEDEMDHWLW4X35JANCNFSM6AAAAAAV7OF5ZA . You are receiving this because you are subscribed to this thread.Message ID: @.***>