| Copyright | (c) Matt Noonan 2018 |
|---|---|
| License | BSD-style |
| Maintainer | matt.noonan@gmail.com |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Theory.Named
Contents
Description
- data Named name a
- type (~~) a name = Named name a
- name :: a -> (forall name. (a ~~ name) -> t) -> t
- name2 :: a -> b -> (forall name1 name2. (a ~~ name1) -> (b ~~ name2) -> t) -> t
- name3 :: a -> b -> c -> (forall name1 name2 name3. (a ~~ name1) -> (b ~~ name2) -> (c ~~ name3) -> t) -> t
- type Defining p = (Coercible p Defn, Coercible Defn p)
- data Defn
- defn :: Defining f => a -> a ~~ f
Named values
A value of type a ~~ name has the same runtime
representation as a value of type a, with a
phantom "name" attached.
name :: a -> (forall name. (a ~~ name) -> t) -> t Source #
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 Source #
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 Source #
Same as name, but names three values at once.
Definitions
type Defining p = (Coercible p Defn, Coercible Defn p) Source #
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.
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