Theory.Named

Named values

data Named name a

A value of type a ~~ name has the same runtime representation as a value of type a, with a phantom "name" attached.

Instances

The (Named name a) a

Methods

the :: Named name a -> a

type (~~) a name = Named name a

An infix alias for Named.

name :: a -> (forall name. (a ~~ name) -> t) -> t

Introduce a name for the argument, and pass the named argument into the given function.

name2 :: a -> b -> (forall name1 name2. (a ~~ name1) -> (b ~~ name2) -> t) -> t

Same as name, but names two values at once.

name3 :: a -> b -> c -> (forall name1 name2 name3. (a ~~ name1) -> (b ~~ name2) -> (c ~~ name3) -> t) -> t

Same as name, but names three values at once.

Definitions

type Defining p = (Coercible p Defn, Coercible Defn p)

The Defining P constraint holds in any module where P has been defined as a newtype wrapper of Defn. It holds only in that module, if the constructor of P is not exported.

data Defn

Library authors can introduce new names in a controlled way by creating newtype wrappers of Defn. The constructor of the newtype should *not* be exported, so that the library can retain control of how the name is introduced.

newtype Bob = Bob Defn

bob :: Int ~~ Bob
bob = defn 42

defn :: Defining f => a -> a ~~ f

In the module where the name f is defined, attach the name f to a value.