Singlethongs

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.

Documentation

data family Sing (a :: k)

class SingI (a :: k) where

Methods

sing :: Sing a

data SomeSing k where

Constructors

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

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

class SingKind k where

Associated Types

type Demote k :: *

Methods

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

toSing :: Demote k -> SomeSing k

Template Haskell

singlethongs :: Name -> Q [Dec]

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

TestEquality ((:~:) a :: k -> Type)

Since: base-4.7.0.0

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

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

TestEquality ((:~:) a :: k -> Type)

Since: base-4.7.0.0

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

Defined in Data.Type.Equality

Methods

minBound :: a :~: b

maxBound :: a :~: b

a ~ b => Enum (a :~: b)

Since: base-4.7.0.0

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

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

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

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

Defined in Data.Type.Equality

Methods

showsPrec :: Int -> (a :~: b) -> ShowS

show :: (a :~: b) -> String

showList :: [a :~: b] -> ShowS