Copyright | Copyright (c) 2016 the Hakaru team |
---|---|
License | BSD3 |
Maintainer | wren@community.haskell.org |
Stability | experimental |
Portability | GHC-only |
Safe Haskell | None |
Language | Haskell2010 |
Singleton types for the Hakaru
kind, and a decision procedure
for Hakaru
type-equality.
Synopsis
- data family Sing (a :: k) :: *
- class SingI (a :: k) where
- singOf :: SingI a => proxy a -> Sing a
- sBool :: Sing HBool
- sUnit :: Sing HUnit
- sPair :: Sing a -> Sing b -> Sing (HPair a b)
- sEither :: Sing a -> Sing b -> Sing (HEither a b)
- sList :: Sing a -> Sing (HList a)
- sMaybe :: Sing a -> Sing (HMaybe a)
- sUnMeasure :: Sing (HMeasure a) -> Sing a
- sUnArray :: Sing (HArray a) -> Sing a
- sUnPair :: Sing (HPair a b) -> (Sing a, Sing b)
- sUnPair' :: Sing (x :: Hakaru) -> (forall (a :: Hakaru) (b :: Hakaru). (TypeEq x (HPair a b), Sing a, Sing b) -> r) -> Maybe r
- sUnEither :: Sing (HEither a b) -> (Sing a, Sing b)
- sUnEither' :: Sing (x :: Hakaru) -> (forall (a :: Hakaru) (b :: Hakaru). (TypeEq x (HEither a b), Sing a, Sing b) -> r) -> Maybe r
- sUnList :: Sing (HList a) -> Sing a
- sUnMaybe :: Sing (HMaybe a) -> Sing a
- sUnFun :: Sing (a :-> b) -> (Sing a, Sing b)
- someSSymbol :: String -> (forall s. Sing (s :: Symbol) -> k) -> k
- ssymbolVal :: forall s. Sing (s :: Symbol) -> String
- sSymbol_Bool :: Sing "Bool"
- sSymbol_Unit :: Sing "Unit"
- sSymbol_Pair :: Sing "Pair"
- sSymbol_Either :: Sing "Either"
- sSymbol_List :: Sing "List"
- sSymbol_Maybe :: Sing "Maybe"
Documentation
data family Sing (a :: k) :: * infixr 7 `SEt`infixr 6 `SPlus`infixr 0 `SFun` Source #
The data families of singletons for each kind.
Instances
JmEq1 (Sing :: Symbol -> *) Source # | |
JmEq1 (Sing :: HakaruCon -> *) Source # | |
JmEq1 (Sing :: HakaruFun -> *) Source # | |
JmEq1 (Sing :: Hakaru -> *) Source # | |
JmEq1 (Sing :: Untyped -> *) Source # | |
Eq1 (Sing :: Symbol -> *) Source # | |
Eq1 (Sing :: HakaruCon -> *) Source # | |
Eq1 (Sing :: HakaruFun -> *) Source # | |
Eq1 (Sing :: Hakaru -> *) Source # | |
Eq1 (Sing :: Untyped -> *) Source # | |
Show1 (Sing :: Symbol -> *) Source # | |
Show1 (Sing :: HakaruCon -> *) Source # | |
Show1 (Sing :: HakaruFun -> *) Source # | |
Show1 (Sing :: Hakaru -> *) Source # | |
Show1 (Sing :: Untyped -> *) Source # | |
Coerce (Sing :: Hakaru -> *) Source # | |
PrimCoerce (Sing :: Hakaru -> *) Source # | |
primCoerceTo :: PrimCoercion a b -> Sing a -> Sing b Source # primCoerceFrom :: PrimCoercion a b -> Sing b -> Sing a Source # | |
JmEq1 (Sing :: [[HakaruFun]] -> *) Source # | |
JmEq1 (Sing :: [HakaruFun] -> *) Source # | |
Eq1 (Sing :: [[HakaruFun]] -> *) Source # | |
Eq1 (Sing :: [HakaruFun] -> *) Source # | |
Show1 (Sing :: [[HakaruFun]] -> *) Source # | |
Show1 (Sing :: [HakaruFun] -> *) Source # | |
Eq (Sing a) Source # | |
Eq (Sing a) Source # | |
Eq (Sing s) Source # | |
Eq (Sing a) Source # | |
Eq (Sing a) Source # | |
Eq (Sing a) Source # | |
Eq (Sing a) # | |
Show (Sing a) Source # | |
Show (Sing a) Source # | |
Show (Sing s) Source # | |
Show (Sing a) Source # | |
Show (Sing a) Source # | |
Show (Sing a) Source # | |
Show (Sing a) # | |
TCMTypeRepr (Sing x) Source # | |
data Sing (s :: Symbol) Source # | N.B., in order to bring the |
data Sing (a :: HakaruCon) Source # | |
data Sing (a :: HakaruFun) Source # | |
data Sing (a :: Hakaru) Source # | Singleton types for the kind of Hakaru types. We need to use
this instead of |
data Sing (a :: Untyped) Source # | |
data Sing (a :: [[HakaruFun]]) Source # | |
data Sing (a :: [HakaruFun]) Source # | |
class SingI (a :: k) where Source #
A class for automatically generating the singleton for a given Hakaru type.
Instances
KnownSymbol s => SingI (s :: Symbol) Source # | |
SingI I Source # | |
SingI HNat Source # | |
SingI HInt Source # | |
SingI HProb Source # | |
SingI HReal Source # | |
SingI U Source # | |
KnownSymbol s => SingI (TyCon s :: HakaruCon) Source # | |
SingI a => SingI (K a :: HakaruFun) Source # | |
SingI a => SingI (HMeasure a :: Hakaru) Source # | |
SingI a => SingI (HArray a :: Hakaru) Source # | |
(SingI a, SingI b) => SingI (a :@ b :: HakaruCon) Source # | |
(SingI a, SingI b) => SingI (a :-> b :: Hakaru) Source # | |
(sop ~ Code t, SingI t, SingI sop) => SingI (HData t sop :: Hakaru) Source # | |
SingI ([] :: [[HakaruFun]]) Source # | |
SingI ([] :: [HakaruFun]) Source # | |
(SingI xs, SingI xss) => SingI (xs ': xss :: [[HakaruFun]]) Source # | |
(SingI x, SingI xs) => SingI (x ': xs :: [HakaruFun]) Source # | |
Some helpful shorthands for "built-in" datatypes
Constructing singletons
Destructing singletons
sUnPair' :: Sing (x :: Hakaru) -> (forall (a :: Hakaru) (b :: Hakaru). (TypeEq x (HPair a b), Sing a, Sing b) -> r) -> Maybe r Source #
sUnEither' :: Sing (x :: Hakaru) -> (forall (a :: Hakaru) (b :: Hakaru). (TypeEq x (HEither a b), Sing a, Sing b) -> r) -> Maybe r Source #
Singletons for Symbol
sSymbol_Bool :: Sing "Bool" Source #
sSymbol_Unit :: Sing "Unit" Source #
sSymbol_Pair :: Sing "Pair" Source #
sSymbol_Either :: Sing "Either" Source #
sSymbol_List :: Sing "List" Source #
sSymbol_Maybe :: Sing "Maybe" Source #