!PLH      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGSafe &'-HSUVX dependent-sumH0-like class for 1-type-parameter GADTs. Unlike 3, this one cannot be mechanically derived from a H instance because , must choose the phantom type based on the I being parsed. dependent-sumGReadS 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) dependent-sumJ)-like class for 1-type-parameter GADTs. GShow t => ..." is equivalent to something like (forall a. Show (t a)) => ...R. 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 dependent-sumKgreadMaybe "InL Refl" mkSome :: Maybe (Some (Sum ((:~:) Int) ((:~:) Bool)))Just (Some (InL Refl))7greadMaybe "garbage" mkSome :: Maybe (Some ((:~:) Int))Nothing dependent-sum=gshow (Pair Refl Refl :: Product ((:~:) Int) ((:~:) Int) Int)"Pair Refl Refl" dependent-sum4gshow (InL Refl :: Sum ((:~:) Int) ((:~:) Bool) Int) "InL Refl"     Safe&'-2=>?HSUVX,= dependent-sumType class for comparable GADT-like structures. When 2 things are equal, must return a witness that their parameter types are equal as well (). dependent-sumA 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. dependent-sumA class for type-contexts which contain enough information to (at least in some cases) decide the equality of types occurring within them. dependent-sum2Produce a witness of type-equality, if one exists.NA handy idiom for using this would be to pattern-bind in the Maybe monad, eg.: pextract :: GEq tag => tag a -> DSum tag -> Maybe a extract t1 (t2 :=> x) = do Refl <- geq t1 t2 return xOr in a list comprehension: extractMany :: GEq tag => tag a -> [DSum tag] -> [a] extractMany t1 things = [ x | (t2 :=> x) <- things, Refl <- maybeToList (geq t1 t2)](Making use of the DSum type from Data.Dependent.Sum in both examples) dependent-sumJBackwards compatibility alias; as of GHC 7.8, this is the same as `(:~:)`. dependent-sumIf f has a L instance, this function makes a suitable default implementation of '(==)'. dependent-sumIf f has a L instance, this function makes a suitable default implementation of '(/=)'.  dependent-sumTODO: Think of a better name.This operation forgets the phantom types of a  value. ! !Safe&',-=>?@AEHUVXk?=3 dependent-sumA 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 Int6Then, we have the following valid expressions of type Applicative f => DSum Tag f: #AString ==> "hello!" AnInt ==> 42(And we can write functions that consume  DSum Tag f values by matching, such as: toString :: DSum Tag Identity -> String toString (AString :=> Identity str) = str toString (AnInt :=> Identity int) = show intBy analogy to the (key => value) construction for dictionary entries in many dynamic languages, we use (key :=> value) as the constructor for dependent sums. The :=> and ==> operators have very low precedence and bind to the right, so if the Tag2 GADT is extended with an additional constructor Rec :: Tag (DSum Tag Identity), then Rec ==> AnInt ==> 3 + 4" is parsed as would be expected (Rec ==> (AnInt ==> (3 + 4))) and has type DSum Identity Tag(. Its precedence is just above that of K, so foo bar $ AString ==> "eep" is equivalent to foo bar (AString ==> "eep"). /0123456789 345261708/94151 Trustworthy %&'-HSXgLX> dependent-sum>Existential. This is type is useful to hide GADTs' parameters.?data Tag :: * -> * where TagInt :: Tag Int; TagBool :: Tag Booloinstance GShow Tag where gshowsPrec _ TagInt = showString "TagInt"; gshowsPrec _ TagBool = showString "TagBool"You can either use PatternSynonymslet x = Some TagIntx Some TagInt?case x of { Some TagInt -> "I"; Some TagBool -> "B" } :: String"I"or you can use functionslet y = mkSome TagBooly Some TagBoolJwithSome y $ \y' -> case y' of { TagInt -> "I"; TagBool -> "B" } :: String"B"The implementation of C is safe.?let f :: Tag a -> Tag a; f TagInt = TagInt; f TagBool = TagBool mapSome f y Some TagBoolbut you can also use:withSome y (mkSome . f) Some TagBoolA dependent-sum Constructor.B dependent-sum Eliminator.>@?ABC>@?@?ABCL       !"#$%&'()*+,-./0123456789:;<=>?@ABCDEDFGHIJKLMNOPQROST(dependent-sum-0.6-1PGS2a4hBAnHwbRM9HUUuOData.GADT.CompareData.GADT.ShowData.Dependent.Sum Data.SomebaseData.Type.EqualityRefl:~:GRead greadsPrecGReadS GReadResultgetGReadResultGShow gshowsPrecgshowsgshowgreadsgread greadMaybe$fGShowkProduct $fGShowkSum$fGShowkTypeRep $fGShowk:~: $fGReadkSum $fGReadk:~:GComparegcompare GOrderingGLTGEQGGTGEqgeq:= defaultEq defaultNeqweakenOrderingdefaultCompare $fGEqkTypeRep $fGEqkProduct $fGEqkSum $fGEqk:~:$fGReadkGOrdering$fGShowkGOrdering$fShowGOrdering$fOrdGOrdering $fEqGOrdering$fGComparekProduct$fGComparekSum$fGComparekTypeRep$fGComparek:~:OrdTagEqTagReadTagShowTagDSum:=>==>showTaggedPrecreadTaggedPrec eqTaggedPreccompareTaggedPrec $fOrdDSum$fEqDSum $fReadDSum $fShowDSumSomeThismkSomewithSomemapSome $fOrdSome$fEqSome $fReadSome $fShowSomeGHC.ReadReadGHC.BaseStringGHC.ShowShow$