Data.Parameterized.WithRepr

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

Turn an explicit Repr value into an implict KnownRepr constraint

Minimal complete definition

Nothing

Methods

withRepr :: f a -> (KnownRepr f a => r) -> r

Instances

IsRepr BoolRepr

Defined in Data.Parameterized.WithRepr

Methods

withRepr :: forall (a :: k) r. BoolRepr a -> (KnownRepr BoolRepr a => r) -> r

IsRepr NatRepr

Defined in Data.Parameterized.WithRepr

Methods

withRepr :: forall (a :: k) r. NatRepr a -> (KnownRepr NatRepr a => r) -> r

IsRepr SymbolRepr

Defined in Data.Parameterized.WithRepr

Methods

withRepr :: forall (a :: k) r. SymbolRepr a -> (KnownRepr SymbolRepr a => r) -> r

IsRepr PeanoRepr

Defined in Data.Parameterized.WithRepr

Methods

withRepr :: forall (a :: k) r. PeanoRepr a -> (KnownRepr PeanoRepr a => r) -> r

IsRepr f => IsRepr (List f :: [k] -> Type)

Defined in Data.Parameterized.WithRepr

Methods

withRepr :: forall (a :: k0) r. List f a -> (KnownRepr (List f) a => r) -> r

IsRepr f => IsRepr (Assignment f :: Ctx k -> Type)

Defined in Data.Parameterized.WithRepr

Methods

withRepr :: forall (a :: k0) r. Assignment f a -> (KnownRepr (Assignment f) a => r) -> r