{-| Copyright : (c) Galois, Inc 2014-2019 Maintainer : Joe Hendrix <jhendrix@galois.com> Description : a type family for representing a type-level string (AKA symbol) at runtime 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. -} {-# LANGUAGE DataKinds #-} {-# LANGUAGE ExplicitNamespaces #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE Trustworthy #-} module Data.Parameterized.SymbolRepr ( -- * SymbolRepr SymbolRepr , symbolRepr , knownSymbol , someSymbol -- * Re-exports , type GHC.Symbol , GHC.KnownSymbol ) where import GHC.TypeLits as GHC import Unsafe.Coerce (unsafeCoerce) import Data.Hashable import Data.Proxy import qualified Data.Text as Text import Data.Parameterized.Classes import Data.Parameterized.Some -- | A runtime representation of a GHC type-level symbol. newtype SymbolRepr (nm::GHC.Symbol) = SymbolRepr { symbolRepr :: Text.Text -- ^ The underlying text representation of the symbol } -- INVARIANT: The contained runtime text value matches the value -- of the type level symbol. The SymbolRepr constructor -- is not exported so we can maintain this invariant in this -- module. -- | Generate a symbol representative at runtime. The type-level -- symbol will be abstract, as it is hidden by the 'Some' constructor. someSymbol :: Text.Text -> Some SymbolRepr someSymbol nm = Some (SymbolRepr nm) -- | Generate a value representative for the type level symbol. knownSymbol :: GHC.KnownSymbol s => SymbolRepr s knownSymbol = go Proxy where go :: GHC.KnownSymbol s => Proxy s -> SymbolRepr s go p = SymbolRepr $! packSymbol (GHC.symbolVal p) -- NOTE here we explicitly test that unpacking the packed text value -- gives the desired string. This is to avoid pathological corner cases -- involving string values that have no text representation. packSymbol str | Text.unpack txt == str = txt | otherwise = error $ "Unrepresentable symbol! "++ str where txt = Text.pack str instance (GHC.KnownSymbol s) => KnownRepr SymbolRepr s where knownRepr = knownSymbol instance TestEquality SymbolRepr where testEquality (SymbolRepr x :: SymbolRepr x) (SymbolRepr y) | x == y = Just (unsafeCoerce (Refl :: x :~: x)) | otherwise = Nothing instance OrdF SymbolRepr where compareF (SymbolRepr x :: SymbolRepr x) (SymbolRepr y) | x < y = LTF | x == y = unsafeCoerce (EQF :: OrderingF x x) | otherwise = GTF -- These instances are trivial by the invariant -- that the contained string matches the type-level -- symbol instance Eq (SymbolRepr x) where _ == _ = True instance Ord (SymbolRepr x) where compare _ _ = EQ instance HashableF SymbolRepr where hashWithSaltF = hashWithSalt instance Hashable (SymbolRepr nm) where hashWithSalt s (SymbolRepr nm) = hashWithSalt s nm instance Show (SymbolRepr nm) where show (SymbolRepr nm) = Text.unpack nm instance ShowF SymbolRepr