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


-- | Dependent sum type
--   
--   Dependent sums and supporting typeclasses for comparing and formatting
--   them.
@package dependent-sum
@version 0.2.0.1

module Data.GADT.Show

-- | <a>Show</a>-like class for 1-type-parameter GADTs
class GShow t
gshowsPrec :: GShow t => Int -> t a -> ShowS
gshows :: GShow t => t a -> ShowS
gshow :: GShow t => t a -> String
type GReadS t = String -> [(forall b. (forall a. t a -> b) -> b, String)]
class GRead t
greadsPrec :: GRead t => Int -> GReadS t
greads :: GRead t => GReadS t
gread :: GRead t => String -> (forall a. t a -> b) -> b

module Data.GADT.Compare

-- | A GADT witnessing equality of two types. Its only inhabitant is
--   <a>Refl</a>.
data (:=) a b
Refl :: a := a

-- | A class for type-contexts which contain enough information to (at
--   least in some cases) decide the equality of types occurring within
--   them.
class GEq f
geq :: GEq f => f a -> f b -> Maybe (a := b)

-- | If <tt>f</tt> has a <a>GEq</a> instance, this function makes a
--   suitable default implementation of '(==)'.
defaultEq :: GEq f => f a -> f b -> Bool

-- | If <tt>f</tt> has a <a>GEq</a> instance, this function makes a
--   suitable default implementation of '(/=)'.
defaultNeq :: GEq f => f a -> f b -> Bool

-- | A type for the result of comparing GADT constructors; the type
--   parameters of the GADT values being compared are included so that in
--   the case where they are equal their parameter types can be unified.
data GOrdering a b
GLT :: GOrdering a b
GEQ :: GOrdering t t
GGT :: GOrdering a b

-- | TODO: Think of a better name
--   
--   This operation forgets the phantom types of a <a>GOrdering</a> value.
weakenOrdering :: GOrdering a b -> Ordering

-- | Type class for orderable GADT-like structures. When 2 things are
--   equal, must return a witness that their parameter types are equal as
--   well (GEQ). |Type class for comparable GADT-like structures. When 2
--   things are equal, must return a witness that their parameter types are
--   equal as well (<a>GEQ</a>).
class GEq f => GCompare f
gcompare :: GCompare f => f a -> f b -> GOrdering a b
instance [safe] Typeable2 :=
instance [safe] Typeable2 GOrdering
instance [safe] GCompare ((:=) a)
instance [safe] GRead (GOrdering a)
instance [safe] GShow (GOrdering a)
instance [safe] Show (GOrdering a b)
instance [safe] Ord (GOrdering a b)
instance [safe] Eq (GOrdering a b)
instance [safe] GEq ((:=) a)
instance [safe] GRead ((:=) a)
instance [safe] Read (a := a)
instance [safe] GShow ((:=) a)
instance [safe] Show (a := b)
instance [safe] Ord (a := b)
instance [safe] Eq (a := b)

module Data.Dependent.Sum

-- | A basic dependent sum type; the first component is a tag that
--   specifies the type of the second; for example, think of a GADT such
--   as:
--   
--   <pre>
--   data Tag a where
--      AString :: Tag String
--      AnInt   :: Tag Int
--   </pre>
--   
--   Then, we have the following valid expressions of type <tt>DSum
--   Tag</tt>:
--   
--   <pre>
--   AString :=&gt; "hello!"
--   AnInt   :=&gt; 42
--   </pre>
--   
--   And we can write functions that consume <tt>DSum Tag</tt> values by
--   matching, such as:
--   
--   <pre>
--   toString :: DSum Tag -&gt; String
--   toString (AString :=&gt; str) = str
--   toString (AnInt   :=&gt; int) = show int
--   </pre>
--   
--   By analogy to the (key =&gt; value) construction for dictionary
--   entries in many dynamic languages, we use (key :=&gt; value) as the
--   constructor for dependent sums. The :=&gt; operator has very low
--   precedence and binds to the right, so if the <tt>Tag</tt> GADT is
--   extended with an additional constructor <tt>Rec :: Tag (DSum
--   Tag)</tt>, then <tt>Rec :=&gt; AnInt :=&gt; 3 + 4</tt> is parsed as
--   would be expected (<tt>Rec :=&gt; (AnInt :=&gt; (3 + 4))</tt>) and has
--   type <tt>DSum Tag</tt>. Its precedence is just above that of <a>$</a>,
--   so <tt>foo bar $ AString :=&gt; <a>eep</a></tt> is equivalent to
--   <tt>foo bar (AString :=&gt; <a>eep</a>)</tt>.
data DSum tag
(:=>) :: !tag a -> a -> DSum tag

-- | In order to make a <a>Show</a> instance for <tt>DSum tag</tt>,
--   <tt>tag</tt> must be able to show itself as well as any value of the
--   tagged type. <a>GShow</a> together with this class provides the
--   interface by which it can do so.
--   
--   <tt>GShow tag =&gt; t</tt> is conceptually equivalent to something
--   like this imaginary syntax: <tt>(forall a. Inhabited (tag a) =&gt;
--   Show a) =&gt; t</tt>, where <tt>Inhabited</tt> is an imaginary
--   predicate that characterizes non-empty types, and <tt>a</tt> does not
--   occur free in <tt>t</tt>.
--   
--   The <tt>Tag</tt> example type introduced in the <a>DSum</a> section
--   could be given the following instances:
--   
--   <pre>
--   instance GShow Tag where
--       gshowsPrec _showsValPrec _p AString = showString "AString"
--       gshowsPrec _showsValPrec _p AnInt   = showString "AnInt"
--   instance ShowTag Tag where
--       showTaggedPrec AString = showsPrec
--       showTaggedPrec AnInt   = showsPrec
--   </pre>
class GShow tag => ShowTag tag
showTaggedPrec :: ShowTag tag => tag a -> Int -> a -> ShowS
class GRead tag => ReadTag tag
readTaggedPrec :: ReadTag tag => tag a -> Int -> ReadS a

-- | In order to test <tt>DSum tag</tt> for equality, <tt>tag</tt> must
--   know how to test both itself and its tagged values for equality.
--   <a>EqTag</a> defines the interface by which they are expected to do
--   so.
--   
--   Continuing the <tt>Tag</tt> example from the <a>DSum</a> section, we
--   can define:
--   
--   <pre>
--   instance GEq Tag where
--       geq AString AString = Just Refl
--       geq AString AnInt   = Nothing
--       geq AnInt   AString = Nothing
--       geq AnInt   AnInt   = Just Refl
--   instance EqTag Tag where
--       eqTagged AString AString = (==)
--       eqTagged AnInt   AnInt   = (==)
--   </pre>
--   
--   Note that <a>eqTagged</a> is not called until after the tags have been
--   compared, so it only needs to consider the cases where <a>gcompare</a>
--   returns <a>GEQ</a>.
class GEq tag => EqTag tag
eqTagged :: EqTag tag => tag a -> tag a -> a -> a -> Bool

-- | In order to compare <tt>DSum tag</tt> values, <tt>tag</tt> must know
--   how to compare both itself and its tagged values. <a>OrdTag</a>
--   defines the interface by which they are expected to do so.
--   
--   Continuing the <tt>Tag</tt> example from the <a>EqTag</a> section, we
--   can define:
--   
--   <pre>
--   instance GCompare Tag where
--       gcompare AString AString = GEQ
--       gcompare AString AnInt   = GLT
--       gcompare AnInt   AString = GGT
--       gcompare AnInt   AnInt   = GEQ
--   instance OrdTag Tag where
--       compareTagged AString AString = compare
--       compareTagged AnInt   AnInt   = compare
--   </pre>
--   
--   As with <a>eqTagged</a>, <a>compareTagged</a> only needs to consider
--   cases where <a>gcompare</a> returns <a>GEQ</a>.
class (EqTag tag, GCompare tag) => OrdTag tag
compareTagged :: OrdTag tag => tag a -> tag a -> a -> a -> Ordering
instance [safe] OrdTag tag => Ord (DSum tag)
instance [safe] Ord a => OrdTag ((:=) a)
instance [safe] EqTag tag => Eq (DSum tag)
instance [safe] Eq a => EqTag ((:=) a)
instance [safe] ReadTag tag => Read (DSum tag)
instance [safe] Read a => ReadTag ((:=) a)
instance [safe] ShowTag tag => Show (DSum tag)
instance [safe] Show a => ShowTag (GOrdering a)
instance [safe] Show a => ShowTag ((:=) a)