Safe Haskell	None
Language	Haskell2010

Singlethongs

Contents

Template Haskell
Re-exports

Description

The goal of the singlethongs library is to offer the bare minimum of what the singletons library offers in a small package that's easy to compile across different GHC versions, including GHCJS.

This module exports a minimal reproduction of what the singletons package offers. Namely Sing, SingI, SomeSing and SingKind, as well as TemplateHaskell support for generating the relevant instances for custom types. If there is some feature that you thing could be added to this library, please suggest it.

The types exported by this module are not the same types as the types as the one exported by the singletons package. Even if they have the same names and implementation, they are not seen as equal by the type-checker. They are only intended to be a drop-in replacement.

Synopsis

data family Sing (a :: k)
class SingI (a :: k) where
- sing :: Sing a
data SomeSing k where
- SomeSing :: Sing (a :: k) -> SomeSing k
withSomeSing :: SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r
class SingKind k where
- type Demote k :: *
- fromSing :: Sing (a :: k) -> Demote k
- toSing :: Demote k -> SomeSing k
singlethongs :: Name -> Q [Dec]
class TestEquality (f :: k -> Type) where
- testEquality :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
data (a :: k) :~: (b :: k) where
- Refl :: forall k (a :: k). a :~: a

Documentation

data family Sing (a :: k) Source #

class SingI (a :: k) where Source #

Methods

sing :: Sing a Source #

data SomeSing k where Source #

Constructors

SomeSing :: Sing (a :: k) -> SomeSing k

withSomeSing :: SingKind k => Demote k -> (forall (a :: k). Sing a -> r) -> r Source #

class SingKind k where Source #

Associated Types

type Demote k :: * Source #

Methods

fromSing :: Sing (a :: k) -> Demote k Source #

toSing :: Demote k -> SomeSing k Source #

Template Haskell

singlethongs :: Name -> Q [Dec] Source #

Generate Sing, SingI, SingKind and TestEquality instances for a datatype.

Given a datatype like Foo below, having one or more unary constructors:

data Foo = Bar | Qux

singlethongs ''Foo

The following code will be generated:

data instance Sing (x :: Foo) where
  SBar :: Sing 'Bar
  SQux :: Sing 'Qux

instance SingKind Fobo where
  type Demote Foo = Foo
  fromSing SBar = Bar
  fromSing SQux = Qux
  toSing Bar = SomeSing SBar
  toSing Qux = SomeSing SQux

instance SingI 'Bar where sing = SBar
instance SingI 'Qux where sing = SQux

instance TestEquality (Sing :: Foo -> *) where
  testEquality SBar SBar = Just Refl
  testEquality SQux SQux = Just Refl
  testEquality _ _ = Nothing

In order to use this singlethongs function, you will need to enable the following GHC extensions:

{-# LANGUAGE DataKinds, GADTs, KindSignatures, TemplateHaskell, TypeFamilies #-}

Re-exports

class TestEquality (f :: k -> Type) 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 :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b) #

Conditionally prove the equality of a and b.

Instances

Instances details

TestEquality ((:~:) a :: k -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #
TestEquality ((:~~:) a :: k -> Type)	Since: base-4.10.0.0
Instance details Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k0) (b :: k0). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) #

data (a :: k) :~: (b :: 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: base-4.7.0.0

Constructors

Refl :: forall k (a :: k). a :~: a

Instances

Instances details

TestEquality ((:~:) a :: k -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #
a ~ b => Bounded (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods minBound :: a :~: b # maxBound :: a :~: b #
a ~ b => Enum (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods succ :: (a :~: b) -> a :~: b # pred :: (a :~: b) -> a :~: b # toEnum :: Int -> a :~: b # fromEnum :: (a :~: b) -> Int # enumFrom :: (a :~: b) -> [a :~: b] # enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] # enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] # enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] #
Eq (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool # (/=) :: (a :~: b) -> (a :~: b) -> Bool #
Ord (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods compare :: (a :~: b) -> (a :~: b) -> Ordering # (<) :: (a :~: b) -> (a :~: b) -> Bool # (<=) :: (a :~: b) -> (a :~: b) -> Bool # (>) :: (a :~: b) -> (a :~: b) -> Bool # (>=) :: (a :~: b) -> (a :~: b) -> Bool # max :: (a :~: b) -> (a :~: b) -> a :~: b # min :: (a :~: b) -> (a :~: b) -> a :~: b #
a ~ b => Read (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods readsPrec :: Int -> ReadS (a :~: b) # readList :: ReadS [a :~: b] # readPrec :: ReadPrec (a :~: b) # readListPrec :: ReadPrec [a :~: b] #
Show (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS # show :: (a :~: b) -> String # showList :: [a :~: b] -> ShowS #