Safe Haskell	None
Language	Haskell2010

Control.Monad.Foil.Telescope

Description

The labelled telescope: a chain of binders, each carrying a label and a payload in the scope before it.

This is the pattern behind a module's parameter block, a record signature, or an algebraic theory: (A : 𝕌) (m : A → A → A) is a two-step telescope whose second payload mentions the first binder. Because a telescope is a pattern (CoSinkable, UnifiablePattern), scope extension, the names of a block, and α-equivalence of blocks come from the pattern machinery, with the payloads compared through AlphaEquiv.

What this module does not fix is what a payload is. The payload type is a parameter, and the operations that need to look inside one, such as the support a dependency closure needs, take the looking function as an argument. A client instantiates the labels and payloads to its own types. To close a declaration over the fields it uses, apply closeOverTelescope and then withThinnedNameBinderList.

Synopsis

data Telescope label (e :: S -> Type) (n :: S) (l :: S) where
- TelescopeEmpty :: forall label (e :: S -> Type) (n :: S). Telescope label e n n
- TelescopeCons :: forall label (e :: S -> Type) (n :: S) (i :: S) (l :: S). label -> e n -> NameBinder n i -> Telescope label e i l -> Telescope label e n l
telescopePayloads :: forall e (l :: S) label (n :: S). (Sinkable e, Distinct l) => Telescope label e n l -> [e l]
payloadsAgree :: forall label (e :: S -> Type) (n :: S) (l :: S) (r :: S). (Sinkable e, AlphaEquiv e, RelMonad Name e, Distinct n) => Scope n -> Telescope label e n l -> Telescope label e n r -> UnifyNameBinders (Telescope label e) n l r -> Bool
data Param label (e :: S -> Type) (l :: S) = Param {
- paramLabel :: label
- paramName :: Name l
- paramType :: e l
}
telescopeParams :: forall (e :: S -> Type) (l :: S) label (n :: S). (Sinkable e, Distinct l) => Telescope label e n l -> [Param label e l]
telescopeBinders :: forall label (e :: S -> Type) (n :: S) (l :: S). Telescope label e n l -> NameBinderList n l
closeOverTelescope :: forall (l :: S) e label. Distinct l => (e l -> NameSet l) -> [Param label e l] -> NameSet l -> NameSet l

Documentation

data Telescope label (e :: S -> Type) (n :: S) (l :: S) where Source #

A labelled telescope: a chain of binders, each carrying a label and a payload in the scope before it.

The payload of a step lives in the scope the steps before it extend to, which is what makes this a telescope rather than a list. For a module's parameters the label is how the parameter is spelled and the payload is its type, so that (A : 𝕌) (m : A → A → A) is a two-step telescope whose second payload mentions the first binder.

See NameBinderList, which this follows almost line for line.

Since: 0.4.0

Constructors

TelescopeEmpty :: forall label (e :: S -> Type) (n :: S). Telescope label e n n
TelescopeCons
Fields :: forall label (e :: S -> Type) (n :: S) (i :: S) (l :: S). label How the step is labelled. -> e n Its payload, in the scope before it. -> NameBinder n i The binder it introduces. -> Telescope label e i l The steps after it. -> Telescope label e n l

Instances

Instances details

Sinkable e => CoSinkable (Telescope label e) Source #	A telescope is a pattern, so the foil's own machinery walks it. `coSinkabilityProof` typechecks only because a payload is sunk by the renaming of the scope before its binder, rather than by the extended one. `withPattern` has to be written out rather than derived. The generic implementation refuses a pattern with a field indexed by a scope, since it would leave a payload that names a refreshed binder pointing at the name that binder used to have. This instance follows the recipe in `transportPayload`: a `PatternTransport` threaded through the traversal, with each payload moved by the transport accumulated before its own binder, that being the scope the payload lives in.
Instance details Defined in Control.Monad.Foil.Telescope Methods coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> Telescope label e n l -> (forall (l' :: S). (Name l -> Name l') -> Telescope label e n' l' -> r) -> r Source # withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> Telescope label e n l -> (forall (o' :: S). DExt o o' => f n l o o' -> Telescope label e o o' -> Scope o' -> r) -> r Source #
(Sinkable e, AlphaEquiv e, RelMonad Name e) => UnifiablePattern (Telescope label e) Source #	Two telescopes unify when their binders line up and their payloads agree. Labels are ignored, which is what α-equivalence should do with a label: a parameter's spelling is no more relevant than a bound variable's. Payloads are not, since two telescopes agreeing on binders may well disagree on types. `unifyPatterns` is the binder-only approximation, which is all a caller without a scope can be given. `unifyPatternsIn` is the real answer, and it is what the library's α-equivalence calls.
Instance details Defined in Control.Monad.Foil.Telescope Methods unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => Telescope label e n l -> Telescope label e n r -> UnifyNameBinders (Telescope label e) n l r Source # unifyPatternsIn :: forall (n :: S) (l :: S) (r :: S). Distinct n => Scope n -> Telescope label e n l -> Telescope label e n r -> UnifyNameBinders (Telescope label e) n l r Source #

telescopePayloads :: forall e (l :: S) label (n :: S). (Sinkable e, Distinct l) => Telescope label e n l -> [e l] Source #

The payloads of a telescope, each moved into its innermost scope.

Sinking is free, so putting them all in one scope costs nothing and lets a renaming be applied to the whole block at once.

Since: 0.4.0

payloadsAgree :: forall label (e :: S -> Type) (n :: S) (l :: S) (r :: S). (Sinkable e, AlphaEquiv e, RelMonad Name e, Distinct n) => Scope n -> Telescope label e n l -> Telescope label e n r -> UnifyNameBinders (Telescope label e) n l r -> Bool Source #

Do the payloads of two telescopes agree, under the way their binders were unified?

The verdict speaks about binders only, so the renaming it prescribes has to be applied before the payloads are compared, which is exactly what alphaEquivScoped does to the body of a scoped term. Comparing them as they stand would report (A : 𝕌) (x : A) and (B : 𝕌) (y : B) as different, since the second payloads name different binders until the first ones have been identified.

Since: 0.4.0

data Param label (e :: S -> Type) (l :: S) Source #

One step of a telescope, with everything about it moved into the innermost scope.

Sinking is free, so this is the convenient form for anything that has to compare parameters with the names of a term checked under all of them.

Since: 0.4.0

Constructors

Param
Fields paramLabel :: label paramName :: Name l paramType :: e l

telescopeParams :: forall (e :: S -> Type) (l :: S) label (n :: S). (Sinkable e, Distinct l) => Telescope label e n l -> [Param label e l] Source #

The steps of a telescope, outermost first.

Since: 0.4.0

telescopeBinders :: forall label (e :: S -> Type) (n :: S) (l :: S). Telescope label e n l -> NameBinderList n l Source #

The chain of binders a telescope forms.

This is nameBinderListOf at a telescope, written out. The general one goes through withPattern and so rebuilds the telescope only to throw it away, which is worth avoiding on the checking path.

Since: 0.4.0

closeOverTelescope Source #

Arguments

:: forall (l :: S) e label. Distinct l
=> (e l -> NameSet l)	The support of a payload.
-> [Param label e l]
-> NameSet l
-> NameSet l

Close a set of parameters under the parameters their payloads need.

Keeping a parameter puts its payload into the result, so whatever that payload mentions has to be kept too. A payload mentions only the parameters before it, so working from the inside out settles it in one pass.

The support of a payload is the caller's to supply, since the library does not know what a payload is. For terms of the free foil it is supportOf.

Since: 0.4.0