singletons-1.0: A framework for generating singleton types

Copyright(C) 2013 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (eir@cis.upenn.edu)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.Types

Description

Defines and exports types that are useful when working with singletons. Some of these are re-exports from Data.Type.Equality.

Synopsis

Documentation

data KProxy t :: * -> *

A concrete, promotable proxy type, for use at the kind level There are no instances for this because it is intended at the kind level only

Constructors

KProxy 

data Proxy t :: k -> *

A concrete, poly-kinded proxy type

Constructors

Proxy 

Instances

Monad (Proxy *) 
Functor (Proxy *) 
Applicative (Proxy *) 
Foldable (Proxy *) 
Traversable (Proxy *) 
Bounded (Proxy k s) 
Enum (Proxy k s) 
Eq (Proxy k s) 
Data t => Data (Proxy * t) 
Ord (Proxy k s) 
Read (Proxy k s) 
Show (Proxy k s) 
Ix (Proxy k s) 
Generic (Proxy * t) 
Monoid (Proxy * s) 
Typeable (k -> *) (Proxy k) 
type Rep (Proxy k t) = D1 D1Proxy (C1 C1_0Proxy U1) 

data a :~: b :: k -> k -> * where infix 4

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Since: 4.7.0.0

Constructors

Refl :: (:~:) k a1 a1 

Instances

TestCoercion k ((:~:) k a) 
TestEquality k ((:~:) k a) 
Typeable (k -> k -> *) ((:~:) k) 
(~) k a b => Bounded ((:~:) k a b) 
(~) k a b => Enum ((:~:) k a b) 
Eq ((:~:) k a b) 
((~) * a b, Data a) => Data ((:~:) * a b) 
Ord ((:~:) k a b) 
(~) k a b => Read ((:~:) k a b) 
Show ((:~:) k a b) 

gcastWith :: (:~:) k a b -> ((~) k a b -> r) -> r

Generalized form of type-safe cast using propositional equality

class TestEquality f where

This class contains types where you can learn the equality of two types from information contained in terms. Typically, only singleton types should inhabit this class.

Methods

testEquality :: f a -> f b -> Maybe ((:~:) k a b)

Conditionally prove the equality of a and b.

Instances

SDecide k (KProxy k) => TestEquality k (Sing k) 
TestEquality k ((:~:) k a) 

type family If cond tru fls :: k

Type-level If. If True a b ==> a; If False a b ==> b

Equations

If k True tru fls = tru 
If k False tru fls = fls