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

Defined in Theory.Named

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. If a newtype wrapper of Defn contains phantom parameters, these parameters should be given the nominal type role; otherwise, library users may be able to use coercions to manipulate library-specific names in a manner not blessed by the library author.

newtype Bob = Bob Defn

bob :: Int ~~ Bob
bob = defn 42

newtype FooOf name = FooOf Defn
type role FooOf nominal -- disallow coerce :: FooOf name1 -> FooOf name2

fooOf :: (Int ~~ name) -> (Int ~~ FooOf name)
fooOf x = defn (the x)

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

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