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

Copyright | (c) Galois Inc 2019
Safe Haskell | None
Language | Haskell2010

Data.Parameterized.WithRepr

Description

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.

Synopsis

- class IsRepr (f :: k -> Type) where
  - withRepr :: forall (a :: k) r. f a -> (KnownRepr f a => r) -> r

# Documentation

class IsRepr (f :: k -> Type) where Source #

Turn an explicit Repr value into an implict KnownRepr constraint

Minimal complete definition

Nothing

Methods

withRepr :: forall (a :: k) r. f a -> (KnownRepr f a => r) -> r Source #

#### Instances

Instances details

IsRepr NatRepr Source # |
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: forall (a :: Nat) r. NatRepr a -> (KnownRepr NatRepr a => r) -> r Source #
IsRepr PeanoRepr Source # |
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: forall (a :: Peano) r. PeanoRepr a -> (KnownRepr PeanoRepr a => r) -> r Source #
IsRepr BoolRepr Source # |
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: forall (a :: Bool) r. BoolRepr a -> (KnownRepr BoolRepr a => r) -> r Source #
IsRepr SymbolRepr Source # |
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: forall (a :: Symbol) r. SymbolRepr a -> (KnownRepr SymbolRepr a => r) -> r Source #
IsRepr f => IsRepr (Assignment f :: Ctx k -> Type) Source # |
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: forall (a :: Ctx k) r. Assignment f a -> (KnownRepr (Assignment f) a => r) -> r Source #
IsRepr f => IsRepr (List f :: [k] -> Type) Source # |
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: forall (a :: [k]) r. List f a -> (KnownRepr (List f) a => r) -> r Source #