Copyright | (c) Justin Le 2017 |
---|---|
License | BSD-3 |
Maintainer | justin@jle.im |
Stability | unstable |
Portability | portable |
Safe Haskell | None |
Language | Haskell2010 |
There's a lot of identical data types between type-combinators and
singetons, as well as similar typeclasses. This module provides
conversion functions between the two (through the TC
typeclass), and
also many appropriate orphan instances.
- class TC f where
- singLength :: Sing as -> Length as
- singSome :: SomeSing k -> Some (Sing :: k -> Type)
- someSing :: Some (Sing :: k -> Type) -> SomeSing k
- singWit1 :: SingInstance a -> Wit1 SingI a
- wit1Sing :: Wit1 SingI a -> SingInstance a
- data family Sing k (a :: k) :: *
- type SN = (Sing :: N -> Type)
- type ZSym0 = Z
- data SSym0 (l :: TyFun N N)
- type SSym1 (t :: N) = S t
Conversion functions
Typeclass for type-combinator types that can be converted to and from singletons.
singLength :: Sing as -> Length as Source #
singWit1 :: SingInstance a -> Wit1 SingI a Source #
Convert a
from singletons into the more generic
representation SingInstance
a
.Wit1
SingI
a
wit1Sing :: Wit1 SingI a -> SingInstance a Source #
Convert the generic representation
from
type-combinators to Wit1
SIngI
a
from singletons.SingInstance
a
Orphan singleton instance for N
data family Sing k (a :: k) :: * #
The singleton kind-indexed data family.
TC [k] (Prod k (Sing k)) Source # | |
TC (Maybe k) (Option k (Sing k)) Source # | |
TC (Either k l) ((:+:) k l (Sing k) (Sing l)) Source # | |
TC (k, l) ((:*:) k l (Sing k) (Sing l)) Source # | |
data Sing Bool | |
data Sing Ordering | |
data Sing Nat | |
data Sing Symbol | |
data Sing () | |
data Sing N # | |
type KnownC k (Sing k) a # | |
type WitnessC ØC (SingI k a) (Sing k a) # | |
data Sing [a] | |
data Sing (Maybe a) | |
data Sing (NonEmpty a) | |
data Sing (Either a b) | |
data Sing (a, b) | |
data Sing ((~>) k1 k2) | |
data Sing (a, b, c) | |
data Sing (a, b, c, d) | |
data Sing (a, b, c, d, e) | |
data Sing (a, b, c, d, e, f) | |
data Sing (a, b, c, d, e, f, g) | |