Copyright | (c) Galois Inc 2019 |
---|---|
Safe Haskell | None |
Language | Haskell2010 |
This module declares a class with a single method that can be used to
derive a KnownRepr
constraint from an explicit Repr
argument.
Clients of this method need only create an empty instance. The default
implementation suffices.
For example, suppose we have defined a Repr
type for Peano
numbers:
data Peano = Z | S Peano data PeanoRepr p where ZRepr :: PeanoRepr Z SRepr :: PeanoRepr p -> PeanoRepr (S p) -- KnownRepr instances
Then the instance for this class
instance IsRepr PeanoRepr
means that functions with KnownRepr
constraints can be used after
pattern matching.
f :: KnownRepr PeanoRepr a => ... example :: PeanoRepr n -> ... example ZRepr = ... example (SRepr (pm::PeanoRepr m)) = ... withRepr pm f ...
NOTE: The type f
must be a *singleton* type--- i.e. for a given
type a
there should be only one value that inhabits 'f a'. If that
is not the case, this operation can be used to subvert coherence.
Credit: the unsafe implementation of withRepr
is taken from the
withSingI
function in the singletons library
http://hackage.haskell.org/package/singletons-2.5.1/. Packaging
this method in a class here makes it more flexible---we do not have to
define a dedicated Sing
type, but can use any convenient singleton
as a Repr
.
NOTE: if this module is compiled without 1, the default method will not be available.
Documentation
class IsRepr (f :: k -> Type) where Source #
Turn an explicit Repr value into an implict KnownRepr constraint
Nothing
Instances
IsRepr BoolRepr Source # | |
IsRepr NatRepr Source # | |
IsRepr SymbolRepr Source # | |
Defined in Data.Parameterized.WithRepr withRepr :: forall (a :: k) r. SymbolRepr a -> (KnownRepr SymbolRepr a => r) -> r Source # | |
IsRepr PeanoRepr Source # | |
IsRepr f => IsRepr (List f :: [k] -> Type) Source # | |
IsRepr f => IsRepr (Assignment f :: Ctx k -> Type) Source # | |
Defined in Data.Parameterized.WithRepr withRepr :: forall (a :: k0) r. Assignment f a -> (KnownRepr (Assignment f) a => r) -> r Source # |