parameterized-utils-1.0.0: Classes and data structures for working with data-kind indexed types

Copyright(c) Galois Inc 2014-2015
MaintainerJoe Hendrix <jhendrix@galois.com>
Safe HaskellTrustworthy
LanguageHaskell98

Data.Parameterized.SymbolRepr

Contents

Description

This defines a type family SymbolRepr for representing a type-level string (AKA symbol) at runtime. This can be used to branch on a type-level value.

The TestEquality and OrdF instances for SymbolRepr are implemented using unsafeCoerce. This should be typesafe because we maintain the invariant that the string value contained in a SymbolRepr value matches its static type.

At the type level, symbols have very few operations, so SymbolRepr correspondingly has very few functions that manipulate them.

Synopsis

SymbolRepr

data SymbolRepr (nm :: Symbol) Source #

A runtime representation of a GHC type-level symbol.

Instances

TestEquality Symbol SymbolRepr Source # 

Methods

testEquality :: f a -> f b -> Maybe ((SymbolRepr :~: a) b) #

HashableF Symbol SymbolRepr Source # 

Methods

hashWithSaltF :: Int -> f tp -> Int Source #

hashF :: f tp -> Int Source #

ShowF Symbol SymbolRepr Source # 

Methods

withShow :: p f -> q tp -> (Show (f tp) -> a) -> a Source #

showF :: f tp -> String Source #

showsF :: f tp -> String -> String Source #

OrdF Symbol SymbolRepr Source # 

Methods

compareF :: ktp x -> ktp y -> OrderingF SymbolRepr x y Source #

leqF :: ktp x -> ktp y -> Bool Source #

ltF :: ktp x -> ktp y -> Bool Source #

geqF :: ktp x -> ktp y -> Bool Source #

gtF :: ktp x -> ktp y -> Bool Source #

KnownSymbol s => KnownRepr Symbol SymbolRepr s Source # 

Methods

knownRepr :: s ctx Source #

Eq (SymbolRepr x) Source # 

Methods

(==) :: SymbolRepr x -> SymbolRepr x -> Bool #

(/=) :: SymbolRepr x -> SymbolRepr x -> Bool #

Ord (SymbolRepr x) Source # 
Show (SymbolRepr nm) Source # 

Methods

showsPrec :: Int -> SymbolRepr nm -> ShowS #

show :: SymbolRepr nm -> String #

showList :: [SymbolRepr nm] -> ShowS #

Hashable (SymbolRepr nm) Source # 

Methods

hashWithSalt :: Int -> SymbolRepr nm -> Int #

hash :: SymbolRepr nm -> Int #

symbolRepr :: SymbolRepr nm -> Text Source #

The underlying text representation of the symbol

knownSymbol :: KnownSymbol s => SymbolRepr s Source #

Generate a value representative for the type level symbol.

someSymbol :: Text -> Some SymbolRepr Source #

Generate a symbol representative at runtime. The type-level symbol will be abstract, as it is hidden by the Some constructor.

Re-exports

data Symbol :: * #

(Kind) This is the kind of type-level symbols. Declared here because class IP needs it

Instances

SingKind Symbol

Since: 4.9.0.0

Associated Types

type DemoteRep Symbol :: *

Methods

fromSing :: Sing Symbol a -> DemoteRep Symbol

KnownSymbol a => SingI Symbol a

Since: 4.9.0.0

Methods

sing :: Sing a a

TestEquality Symbol SymbolRepr # 

Methods

testEquality :: f a -> f b -> Maybe ((SymbolRepr :~: a) b) #

HashableF Symbol SymbolRepr Source # 

Methods

hashWithSaltF :: Int -> f tp -> Int Source #

hashF :: f tp -> Int Source #

ShowF Symbol SymbolRepr Source # 

Methods

withShow :: p f -> q tp -> (Show (f tp) -> a) -> a Source #

showF :: f tp -> String Source #

showsF :: f tp -> String -> String Source #

OrdF Symbol SymbolRepr Source # 

Methods

compareF :: ktp x -> ktp y -> OrderingF SymbolRepr x y Source #

leqF :: ktp x -> ktp y -> Bool Source #

ltF :: ktp x -> ktp y -> Bool Source #

geqF :: ktp x -> ktp y -> Bool Source #

gtF :: ktp x -> ktp y -> Bool Source #

KnownSymbol n => Reifies Symbol n String 

Methods

reflect :: proxy String -> a #

KnownSymbol s => KnownRepr Symbol SymbolRepr s Source # 

Methods

knownRepr :: s ctx Source #

data Sing Symbol 
data Sing Symbol where
type DemoteRep Symbol 
type DemoteRep Symbol = String
type (==) Symbol a b 
type (==) Symbol a b = EqSymbol a b

class KnownSymbol (n :: Symbol) #

This class gives the string associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.

Since: 4.7.0.0

Minimal complete definition

symbolSing