Portability | portable |
---|---|

Stability | experimental |

Maintainer | Edward Kmett <ekmett@gmail.com> |

Safe Haskell | None |

The problem with locally nameless approaches is that original names are
often useful for error reporting, or to allow for the user in an interactive
theorem prover to convey some hint about the domain. A

is a value
`Name`

n b`b`

supplemented with a (discardable) name that may be useful for error
reporting purposes. In particular, this name does not participate in
comparisons for equality.

This module is *not* exported from Bound by default. You need to explicitly
import it, due to the fact that `Name`

is a pretty common term in other
people's code.

- data Name n b = Name n b
- name :: Name n b -> n
- abstractName :: Monad f => (a -> Maybe b) -> f a -> Scope (Name a b) f a
- abstract1Name :: (Monad f, Eq a) => a -> f a -> Scope (Name a ()) f a
- instantiateName :: (Monad f, Comonad n) => (b -> f a) -> Scope (n b) f a -> f a
- instantiate1Name :: Monad f => f a -> Scope n f a -> f a

# Documentation

We track the choice of `Name`

`n`

as a forgettable property that does *not* affect
the result of (`==`

) or `compare`

.

To compare names rather than values, use `(`

instead.
`on`

`compare`

`name`

)

Name n b |

Typeable2 Name | |

Bitraversable Name | |

Bifunctor Name | |

Bifoldable Name | |

Eq2 Name | |

Ord2 Name | |

Show2 Name | |

Read2 Name | |

Functor (Name n) | |

Foldable (Name n) | |

(Functor (Name n), Foldable (Name n)) => Traversable (Name n) | |

Functor (Name n) => Comonad (Name n) | |

Eq1 (Name b) | |

Eq1 (Name b) => Ord1 (Name b) | |

Show b => Show1 (Name b) | |

Read b => Read1 (Name b) | |

Eq b => Eq (Name n b) | |

(Typeable (Name n b), Data n, Data b) => Data (Name n b) | |

(Eq (Name n b), Ord b) => Ord (Name n b) | |

(Read n, Read b) => Read (Name n b) | |

(Show n, Show b) => Show (Name n b) | |

Generic (Name n b) |

abstractName :: Monad f => (a -> Maybe b) -> f a -> Scope (Name a b) f aSource

Abstraction, capturing named bound variables.

abstract1Name :: (Monad f, Eq a) => a -> f a -> Scope (Name a ()) f aSource

Abstract over a single variable

instantiateName :: (Monad f, Comonad n) => (b -> f a) -> Scope (n b) f a -> f aSource

Enter a scope, instantiating all bound variables, but discarding (comonadic) meta data, like its name

instantiate1Name :: Monad f => f a -> Scope n f a -> f aSource

Enter a `Scope`

that binds one (named) variable, instantiating it.

`instantiate1Name`

=`instantiate1`