-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Existential type utilites
--   
--   This package provides utilities for working with existential types.
@package ghost-buster
@version 0.1.1.0


-- | Provides the type <tt>SuchThat</tt>, which encapsulates an
--   existentially quantified type.
module Data.SuchThat

-- | A <tt><a>SuchThat</a> c p</tt> is a <tt>p s</tt>, where <tt>s</tt> is
--   such that it satisfies all of the constraints in <tt>c</tt>. Note that
--   you must always wrap results from pattern-matching on the
--   <tt><a>SuchThat</a></tt> constructor in a <tt><a>SuchThat</a></tt>, or
--   GHC will complain about <tt>s</tt> escaping its scope.
--   
--   Ideally, we would write:
--   
--   <pre>
--   type SuchThat (c :: [k -&gt; Constraint]) (p :: k -&gt; *) = forall s. Constrain c s =&gt; p s
--   </pre>
--   
--   But type synonyms don't work that way
data SuchThat (c :: [k -> Constraint]) (p :: k -> *)
SuchThat :: (p s) -> SuchThat

-- | Inject a value into a <tt><a>SuchThat</a></tt>. It becomes more
--   ambiguous because it throws out the exact type of <tt>s</tt>.
ambiguate :: forall c p s. Constrain c s => p s -> SuchThat c p

-- | Escape from a <tt><a>SuchThat</a></tt> by running a universally
--   quantified continuation.
ambiguously :: forall c p r. (forall s. Constrain c s => p s -> r) -> SuchThat c p -> r

-- | A <tt><a>ForAny</a> f</tt> is an <tt>f</tt> containing some arbitrary
--   values, meaning you can only apply operations that would work <i>for
--   any</i> type of value it contains. This is useful if the type
--   parameter is phantom because it allows you to ignore it. This is
--   called "ghost busting" because it removes the phantom. It can also be
--   used for reading only the <i>structure</i> of something rather than
--   the actual values. For example, <tt><a>ForAny</a> []</tt> is
--   isomorphic to both the natural numbers, and the fixed point of
--   <tt><a>Maybe</a></tt>.
type ForAny = SuchThat '[]

-- | If the type constructor in question is a functor, we can scope out its
--   structure by converting every element to <tt>()</tt>. Note that this
--   is actually the most general way to do this, since the type signature
--   would otherwise be <tt>Functor p =&gt; SuchThat c p -&gt; (forall x. x
--   -&gt; a) -&gt; p a</tt>. That means the output type must be isomorphic
--   to <tt>()</tt> because that is the terminal object in <tt>Hask</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; discoverStructure (ambiguate ['a','b','c'] :: ForAny [])
--   [(),(),()]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; discoverStructure (ambiguate (Just "hi") :: ForAny Maybe)
--   Just ()
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; discoverStructure (ambiguate Nothing :: ForAny Maybe)
--   Nothing
--   </pre>
discoverStructure :: Functor p => SuchThat c p -> p ()

-- | A function between <tt><a>SuchThat</a> c</tt>'s between different type
--   constructors is isomorphic to a natural transformation between those
--   type constructors. This is especially useful if <tt>c ~ '[]</tt>,
--   meaning you have a <tt><a>ForAny</a></tt>.
naturalTransformation :: (forall x. f x -> g x) -> (forall c. SuchThat c f -> SuchThat c g)

-- | The other half of the aforementioned isomorphism. This specialises
--   <tt>c</tt> to <tt>'[<tt>Constains</tt> x]</tt> under the hood.
unNaturalTransformation :: forall f g. (forall c. SuchThat c f -> SuchThat c g) -> (forall x. f x -> g x)

-- | A <tt><a>Some</a> c</tt> is some value that satisfies all the
--   constraints in <tt>c</tt>.
type Some c = SuchThat c Identity

-- | Build a <tt><a>Some</a> c</tt> from some thing that satisfies
--   <tt>c</tt>.
some :: Constrain c a => a -> Some c

-- | A <tt><a>Satisfies</a> x</tt> is a value that satisfies the single
--   constraint x.
type Satisfies x = Some '[x]

-- | A <tt><a>Contains</a> x f</tt> is isomorphic to an <tt>f x</tt>:
--   
--   <pre>
--   containsToRaw :: Contains x f -&gt; f x
--   containsToRaw = ambiguously id
--   </pre>
--   
--   <pre>
--   rawToContains :: f x -&gt; Contains x f
--   rawToContains = ambiguate
--   </pre>
type Contains x = SuchThat '[(~) x]

-- | A type level fold for applying many constraints to the same thing
