Moduledependent-sum-0.6.2.0Haskell98

Data.GADT.Show

2 types
2 classes
5 values

Packagedependent-sum-0.6.2.0
Exports9
LanguageHaskell98
LicenceLicenseRef-PublicDomain
SourceShow.hs

Example1 expression

>>> import Data.Some

classclass GShow (t :: k -> Type) where

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

Instances5GShow

GShow TypeRepDefined in dependent-sum-0.6.2.0 · Data.GADT.Show
GShow (GOrdering a)Defined in dependent-sum-0.6.2.0 · Data.GADT.Compare
GShow ((:~:) a)Defined in dependent-sum-0.6.2.0 · Data.GADT.Show
(GShow a, GShow b) => GShow (Product a b)Defined in dependent-sum-0.6.2.0 · Data.GADT.Show
Example1 expression
```
>>> gshow (Pair Refl Refl :: Product ((:~:) Int) ((:~:) Int) Int)"Pair Refl Refl"
```
(GShow a, GShow b) => GShow (Sum a b)Defined in dependent-sum-0.6.2.0 · Data.GADT.Show
Example1 expression
```
>>> gshow (InL Refl :: Sum ((:~:) Int) ((:~:) Bool) Int)"InL Refl"
```

valuegshows :: GShow t => t a -> ShowS

valuegshow :: GShow t => t a -> String

newtypenewtype GReadResult (t :: k -> Type)

Constructors

GReadResult
- getGReadResult :: forall b. (forall (a :: k). t a -> b) -> b

typetype GReadS (t :: k -> Type) = String -> [(GReadResult t, 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)

classclass GRead (t :: k -> Type) where

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

Instances3GRead

GRead (GOrdering a)Defined in dependent-sum-0.6.2.0 · Data.GADT.Compare
GRead ((:~:) a)Defined in dependent-sum-0.6.2.0 · Data.GADT.Show
(GRead a, GRead b) => GRead (Sum a b)Defined in dependent-sum-0.6.2.0 · Data.GADT.Show

valuegreads :: GRead t => GReadS t

valuegread :: GRead t => String -> (forall (a :: k). t a -> b) -> b

valuegreadMaybe :: GRead t => String -> (forall (a :: k). t a -> b) -> Maybe b

Example1 expression

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

Example1 expression

>>> greadMaybe "garbage" mkSome :: Maybe (Some ((:~:) Int))Nothing