Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data FormatUn
- data FormatGz
- data Format a where
- data Formats a b where
- data HasFormat a b where
- hasFormatAbsurd :: HasFormat () f -> a
- hasFormatGet :: HasFormat fs f -> Format f
- formatsMap :: (forall f. Format f -> a -> b) -> Formats fs a -> Formats fs b
- formatsMember :: Format f -> Formats fs a -> Maybe (HasFormat fs f)
- formatsLookup :: HasFormat fs f -> Formats fs a -> a
Formats
Type level
Term level
Format is a singleton type (reflection type to term level)
NOTE: In the future we might add further compression formats.
data Formats a b where Source #
Available formats
Rather than having a general list here, we enumerate all possibilities. This means we are very precise about what we expect, and we avoid any runtime errors about unexpected format definitions.
NOTE: If we add additional cases here (for dealing with additional formats)
all calls to error "inaccessible"
need to be reevaluated.
FsNone :: forall b. Formats () b | |
FsUn :: forall b. b -> Formats (FormatUn :- ()) b | |
FsGz :: forall b. b -> Formats (FormatGz :- ()) b | |
FsUnGz :: forall b. b -> b -> Formats (FormatUn :- (FormatGz :- ())) b |
Key membership
data HasFormat a b where Source #
HasFormat fs f
is a proof that f
is a key in fs
.
See formatsMember
and formatsLookup
for typical usage.
HFZ :: forall b fs. Format b -> HasFormat (b :- fs) b | |
HFS :: forall fs b f'. HasFormat fs b -> HasFormat (f' :- fs) b |
Utility
hasFormatAbsurd :: HasFormat () f -> a Source #
hasFormatGet :: HasFormat fs f -> Format f Source #
Map-like operations
formatsLookup :: HasFormat fs f -> Formats fs a -> a Source #