dependent-sum-0.6: Dependent sum type

Safe HaskellSafe
LanguageHaskell98

Data.GADT.Show

Synopsis

Documentation

>>> import Data.Some

class GShow t where Source #

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

Methods

gshowsPrec :: Int -> t a -> ShowS Source #

Instances
GShow (TypeRep :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Show

Methods

gshowsPrec :: Int -> TypeRep a -> ShowS Source #

GShow ((:~:) a :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Show

Methods

gshowsPrec :: Int -> (a :~: a0) -> ShowS Source #

GShow (GOrdering a :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Compare

Methods

gshowsPrec :: Int -> GOrdering a a0 -> ShowS Source #

(GShow a, GShow b) => GShow (Product a b :: k -> Type) Source #
>>> gshow (Pair Refl Refl :: Product ((:~:) Int) ((:~:) Int) Int)
"Pair Refl Refl"
Instance details

Defined in Data.GADT.Show

Methods

gshowsPrec :: Int -> Product a b a0 -> ShowS Source #

(GShow a, GShow b) => GShow (Sum a b :: k -> Type) Source #
>>> gshow (InL Refl :: Sum ((:~:) Int) ((:~:) Bool) Int)
"InL Refl"
Instance details

Defined in Data.GADT.Show

Methods

gshowsPrec :: Int -> Sum a b a0 -> ShowS Source #

gshows :: GShow t => t a -> ShowS Source #

gshow :: GShow t => t a -> String Source #

newtype GReadResult t Source #

Constructors

GReadResult 

Fields

type GReadS t = String -> [(GReadResult t, String)] Source #

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)

class GRead t where Source #

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.

Methods

greadsPrec :: Int -> GReadS t Source #

Instances
GRead ((:~:) a :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Show

Methods

greadsPrec :: Int -> GReadS ((:~:) a) Source #

GRead (GOrdering a :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Compare

(GRead a, GRead b) => GRead (Sum a b :: k -> Type) Source # 
Instance details

Defined in Data.GADT.Show

Methods

greadsPrec :: Int -> GReadS (Sum a b) Source #

gread :: GRead t => String -> (forall a. t a -> b) -> b Source #

greadMaybe :: GRead t => String -> (forall a. t a -> b) -> Maybe b Source #

>>> greadMaybe "InL Refl" mkSome :: Maybe (Some (Sum ((:~:) Int) ((:~:) Bool)))
Just (Some (InL Refl))
>>> greadMaybe "garbage" mkSome :: Maybe (Some ((:~:) Int))
Nothing