-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Dependent sum type -- -- A dependent sum is a generalization of a particular way of thinking -- about the Either type. Either a b can be thought of -- as a 2-tuple (tag, value), where the value of the tag -- determines the type of the value. In particular, either tag = -- Left and value :: a or tag = Right and -- value :: b. -- -- This package allows you to define your own dependent sum types by -- using your own "tag" types. @package dependent-sum @version 0.2.1.0 module Data.GADT.Show -- | Show-like class for 1-type-parameter GADTs. GShow t => -- ... is equivalent to something like (forall a. Show (t a)) -- => .... The easiest way to create instances would probably be -- to write (or derive) an instance Show (T a), and then simply -- say: -- -- 
--   instance GShow t where gshowsPrec = showsPrec
--
class GShow t gshowsPrec :: GShow t => Int -> t a -> ShowS gshows :: GShow t => t a -> ShowS gshow :: GShow t => t a -> String -- | GReadS t is equivalent to ReadS (forall b. (forall a. t a -- -> b) -> b), which is in turn equivalent to ReadS -- (Exists t) (with data Exists t where Exists :: t a -> -- Exists t) type GReadS t = String -> [(forall b. (forall a. t a -> b) -> b, String)] -- | Read-like class for 1-type-parameter GADTs. Unlike -- GShow, this one cannot be mechanically derived from a -- Read instance because greadsPrec must choose the phantom -- type based on the String being parsed. 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 -- Refl. 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 f has a GEq instance, this function makes a -- suitable default implementation of '(==)'. defaultEq :: GEq f => f a -> f b -> Bool -- | If f has a GEq 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 GOrdering 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 (GEQ). 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] GShow ((:=) a) instance [safe] Read (a := 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: -- -- 
--   data Tag a where
--      AString :: Tag String
--      AnInt   :: Tag Int
--
-- -- Then, we have the following valid expressions of type DSum -- Tag: -- -- 
--   AString :=> "hello!"
--   AnInt   :=> 42
--
-- -- And we can write functions that consume DSum Tag values by -- matching, such as: -- -- 
--   toString :: DSum Tag -> String
--   toString (AString :=> str) = str
--   toString (AnInt   :=> int) = show int
--
-- -- By analogy to the (key => value) construction for dictionary -- entries in many dynamic languages, we use (key :=> value) as the -- constructor for dependent sums. The :=> operator has very low -- precedence and binds to the right, so if the Tag GADT is -- extended with an additional constructor Rec :: Tag (DSum -- Tag), then Rec :=> AnInt :=> 3 + 4 is parsed as -- would be expected (Rec :=> (AnInt :=> (3 + 4))) and has -- type DSum Tag. Its precedence is just above that of $, -- so foo bar $ AString :=> eep is equivalent to -- foo bar (AString :=> eep). data DSum tag (:=>) :: !(tag a) -> a -> DSum tag -- | In order to make a Show instance for DSum tag, -- tag must be able to show itself as well as any value of the -- tagged type. GShow together with this class provides the -- interface by which it can do so. -- -- ShowTag tag => t is conceptually equivalent to something -- like this imaginary syntax: (forall a. Inhabited (tag a) => -- Show a) => t, where Inhabited is an imaginary -- predicate that characterizes non-empty types, and a does not -- occur free in t. -- -- The Tag example type introduced in the DSum section -- could be given the following instances: -- -- 
--   instance GShow Tag where
--       gshowsPrec _p AString = showString "AString"
--       gshowsPrec _p AnInt   = showString "AnInt"
--   instance ShowTag Tag where
--       showTaggedPrec AString = showsPrec
--       showTaggedPrec AnInt   = showsPrec
--
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 DSum tag for equality, tag must -- know how to test both itself and its tagged values for equality. -- EqTag defines the interface by which they are expected to do -- so. -- -- Continuing the Tag example from the DSum section, we -- can define: -- -- 
--   instance GEq Tag where
--       geq AString AString = Just Refl
--       geq AnInt   AnInt   = Just Refl
--       geq _       _       = Nothing
--   instance EqTag Tag where
--       eqTagged AString AString = (==)
--       eqTagged AnInt   AnInt   = (==)
--
-- -- Note that eqTagged is not called until after the tags have been -- compared, so it only needs to consider the cases where gcompare -- returns GEQ. class GEq tag => EqTag tag eqTagged :: EqTag tag => tag a -> tag a -> a -> a -> Bool -- | In order to compare DSum tag values, tag must know -- how to compare both itself and its tagged values. OrdTag -- defines the interface by which they are expected to do so. -- -- Continuing the Tag example from the EqTag section, we -- can define: -- -- 
--   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
--
-- -- As with eqTagged, compareTagged only needs to consider -- cases where gcompare returns GEQ. 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)