content: {-# LANGUAGE TypeOperators         #-}
  {-# LANGUAGE RankNTypes            #-}
  {-# LANGUAGE ConstraintKinds       #-}
  {-# LANGUAGE FlexibleContexts      #-}
  {-# LANGUAGE FlexibleInstances     #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE PolyKinds             #-}
  {-# LANGUAGE RoleAnnotations       #-}
  
  {-|
    Module      :  Theory.Named
    Copyright   :  (c) Matt Noonan 2018
    License     :  BSD-style
    Maintainer  :  matt.noonan@gmail.com
    Portability :  portable
  -}
  
  module Theory.Named
    ( -- * Named values
      Named, type (~~)
    , name
    , name2, name3
  
    -- ** Definitions
    , Defining
    , Defn
    , defn
    ) where
  
  import Data.The
  import Data.Coerce
  
  {--------------------------------------------------
    Named values
  --------------------------------------------------}
  
  -- | A value of type @a ~~ name@ has the same runtime
  --   representation as a value of type @a@, with a
  --   phantom "name" attached.
  newtype Named name a = Named a
  type role Named nominal nominal
  
  -- | An infix alias for 'Named'.
  type a ~~ name = Named name a
  
  instance The (Named name a) a
  
  -- | Introduce a name for the argument, and pass the
  --   named argument into the given function.
  name :: a -> (forall name. a ~~ name -> t) -> t
  name x k = k (coerce x)
  
  -- | Same as 'name', but names two values at once.
  name2 :: a -> b -> (forall name1 name2. (a ~~ name1) -> (b ~~ name2) -> t) -> t
  name2 x y k = k (coerce x) (coerce y)
  
  -- | Same as 'name', but names three values at once.
  name3 :: a -> b -> c -> (forall name1 name2 name3. (a ~~ name1) -> (b ~~ name2) -> (c ~~ name3) -> t) -> t
  name3 x y z k = k (coerce x) (coerce y) (coerce z)
  
  
  {--------------------------------------------------
    Definitions
  --------------------------------------------------}
  
  {-| 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)
  @
  -}
  data Defn = Defn
  
  -- | 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.
  type Defining p = (Coercible p Defn, Coercible Defn p)
  
  -- | In the module where the name @f@ is defined, attach the
  --   name @f@ to a value.
  defn :: Defining f => a -> (a ~~ f)
  defn = coerce
  