Copyright	Copyright (c) 2016 the Hakaru team
License	BSD3
Maintainer	wren@community.haskell.org
Stability	experimental
Portability	GHC-only
Safe Haskell	None
Language	Haskell2010

Language.Hakaru.Types.Sing

Contents

Some helpful shorthands for "built-in" datatypes

Description

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
- sing :: Sing a
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

Instances details

JmEq1 (Sing :: Symbol -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods jmEq1 :: forall (i :: k) (j :: k). Sing i -> Sing j -> Maybe (TypeEq i j) Source #
JmEq1 (Sing :: HakaruCon -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods jmEq1 :: forall (i :: k) (j :: k). Sing i -> Sing j -> Maybe (TypeEq i j) Source #
JmEq1 (Sing :: HakaruFun -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods jmEq1 :: forall (i :: k) (j :: k). Sing i -> Sing j -> Maybe (TypeEq i j) Source #
JmEq1 (Sing :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods jmEq1 :: forall (i :: k) (j :: k). Sing i -> Sing j -> Maybe (TypeEq i j) Source #
JmEq1 (Sing :: Untyped -> Type) Source #
Instance details Defined in Language.Hakaru.Parser.AST Methods jmEq1 :: forall (i :: k) (j :: k). Sing i -> Sing j -> Maybe (TypeEq i j) Source #
Eq1 (Sing :: Symbol -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods eq1 :: forall (i :: k). Sing i -> Sing i -> Bool Source #
Eq1 (Sing :: HakaruCon -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods eq1 :: forall (i :: k). Sing i -> Sing i -> Bool Source #
Eq1 (Sing :: HakaruFun -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods eq1 :: forall (i :: k). Sing i -> Sing i -> Bool Source #
Eq1 (Sing :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods eq1 :: forall (i :: k). Sing i -> Sing i -> Bool Source #
Eq1 (Sing :: Untyped -> Type) Source #
Instance details Defined in Language.Hakaru.Parser.AST Methods eq1 :: forall (i :: k). Sing i -> Sing i -> Bool Source #
Show1 (Sing :: Symbol -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods showsPrec1 :: forall (i :: k). Int -> Sing i -> ShowS Source # show1 :: forall (i :: k). Sing i -> String Source #
Show1 (Sing :: HakaruCon -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods showsPrec1 :: forall (i :: k). Int -> Sing i -> ShowS Source # show1 :: forall (i :: k). Sing i -> String Source #
Show1 (Sing :: HakaruFun -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods showsPrec1 :: forall (i :: k). Int -> Sing i -> ShowS Source # show1 :: forall (i :: k). Sing i -> String Source #
Show1 (Sing :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods showsPrec1 :: forall (i :: k). Int -> Sing i -> ShowS Source # show1 :: forall (i :: k). Sing i -> String Source #
Show1 (Sing :: Untyped -> Type) Source #
Instance details Defined in Language.Hakaru.Parser.AST Methods showsPrec1 :: forall (i :: k). Int -> Sing i -> ShowS Source # show1 :: forall (i :: k). Sing i -> String Source #
Coerce (Sing :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Coercion Methods coerceTo :: forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> Sing a -> Sing b Source # coerceFrom :: forall (a :: Hakaru) (b :: Hakaru). Coercion a b -> Sing b -> Sing a Source #
PrimCoerce (Sing :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Coercion Methods primCoerceTo :: forall (a :: Hakaru) (b :: Hakaru). PrimCoercion a b -> Sing a -> Sing b Source # primCoerceFrom :: forall (a :: Hakaru) (b :: Hakaru). PrimCoercion a b -> Sing b -> Sing a Source #
JmEq1 (Sing :: [[HakaruFun]] -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods jmEq1 :: forall (i :: k) (j :: k). Sing i -> Sing j -> Maybe (TypeEq i j) Source #
JmEq1 (Sing :: [HakaruFun] -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods jmEq1 :: forall (i :: k) (j :: k). Sing i -> Sing j -> Maybe (TypeEq i j) Source #
Eq1 (Sing :: [[HakaruFun]] -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods eq1 :: forall (i :: k). Sing i -> Sing i -> Bool Source #
Eq1 (Sing :: [HakaruFun] -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods eq1 :: forall (i :: k). Sing i -> Sing i -> Bool Source #
Show1 (Sing :: [[HakaruFun]] -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods showsPrec1 :: forall (i :: k). Int -> Sing i -> ShowS Source # show1 :: forall (i :: k). Sing i -> String Source #
Show1 (Sing :: [HakaruFun] -> Type) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods showsPrec1 :: forall (i :: k). Int -> Sing i -> ShowS Source # show1 :: forall (i :: k). Sing i -> String Source #
Eq (Sing a) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods (==) :: Sing a -> Sing a -> Bool # (/=) :: Sing a -> Sing a -> Bool #
Eq (Sing a) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods (==) :: Sing a -> Sing a -> Bool # (/=) :: Sing a -> Sing a -> Bool #
Eq (Sing s) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods (==) :: Sing s -> Sing s -> Bool # (/=) :: Sing s -> Sing s -> Bool #
Eq (Sing a) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods (==) :: Sing a -> Sing a -> Bool # (/=) :: Sing a -> Sing a -> Bool #
Eq (Sing a) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods (==) :: Sing a -> Sing a -> Bool # (/=) :: Sing a -> Sing a -> Bool #
Eq (Sing a) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods (==) :: Sing a -> Sing a -> Bool # (/=) :: Sing a -> Sing a -> Bool #
Eq (Sing a) Source #
Instance details Defined in Language.Hakaru.Parser.AST Methods (==) :: Sing a -> Sing a -> Bool # (/=) :: Sing a -> Sing a -> Bool #
Show (Sing a) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods showsPrec :: Int -> Sing a -> ShowS # show :: Sing a -> String # showList :: [Sing a] -> ShowS #
Show (Sing a) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods showsPrec :: Int -> Sing a -> ShowS # show :: Sing a -> String # showList :: [Sing a] -> ShowS #
Show (Sing s) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods showsPrec :: Int -> Sing s -> ShowS # show :: Sing s -> String # showList :: [Sing s] -> ShowS #
Show (Sing a) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods showsPrec :: Int -> Sing a -> ShowS # show :: Sing a -> String # showList :: [Sing a] -> ShowS #
Show (Sing a) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods showsPrec :: Int -> Sing a -> ShowS # show :: Sing a -> String # showList :: [Sing a] -> ShowS #
Show (Sing a) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods showsPrec :: Int -> Sing a -> ShowS # show :: Sing a -> String # showList :: [Sing a] -> ShowS #
Show (Sing a) Source #
Instance details Defined in Language.Hakaru.Parser.AST Methods showsPrec :: Int -> Sing a -> ShowS # show :: Sing a -> String # showList :: [Sing a] -> ShowS #
TCMTypeRepr (Sing x) Source #
Instance details Defined in Language.Hakaru.Syntax.TypeCheck.Unification Methods toTypeRepr :: Sing x -> Maybe (Either Text (Some1 Sing)) Source #
data Sing (s :: Symbol) Source #	N.B., in order to bring the `KnownSymbol` dictionary into scope, you need to pattern match on the `SingSymbol` constructor (similar to when we need to match on `Refl` explicitly). In general you'll want to do this with an at-pattern so that you can also have a variable name for passing the value around (e.g. to be used as an argument to `symbolVal`).
Instance details Defined in Language.Hakaru.Types.Sing data Sing (s :: Symbol) where SingSymbol :: forall (s :: Symbol). KnownSymbol s => Sing s
data Sing (a :: HakaruCon) Source #
Instance details Defined in Language.Hakaru.Types.Sing data Sing (a :: HakaruCon) where STyCon :: forall (s :: Symbol). !(Sing s) -> Sing ('TyCon s) STyApp :: forall (a :: HakaruCon) (b :: Hakaru). !(Sing a) -> !(Sing b) -> Sing (a :@ b)
data Sing (a :: HakaruFun) Source #
Instance details Defined in Language.Hakaru.Types.Sing data Sing (a :: HakaruFun) where SIdent :: Sing 'I SKonst :: forall (a :: Hakaru). !(Sing a) -> Sing ('K a)
data Sing (a :: Hakaru) Source #	Singleton types for the kind of Hakaru types. We need to use this instead of `Proxy` in order to implement `jmEq1`.
Instance details Defined in Language.Hakaru.Types.Sing data Sing (a :: Hakaru) where SNat :: Sing 'HNat SInt :: Sing 'HInt SProb :: Sing 'HProb SReal :: Sing 'HReal SMeasure :: forall (a :: Hakaru). !(Sing a) -> Sing ('HMeasure a) SArray :: forall (a :: Hakaru). !(Sing a) -> Sing ('HArray a) SFun :: forall (a :: Hakaru) (b :: Hakaru). !(Sing a) -> !(Sing b) -> Sing (a :-> b) SData :: forall (t :: HakaruCon). !(Sing t) -> !(Sing (Code t)) -> Sing (HData' t)
data Sing (a :: Untyped) Source #
Instance details Defined in Language.Hakaru.Parser.AST data Sing (a :: Untyped) where SU :: Sing 'U
data Sing (a :: [[HakaruFun]]) Source #
Instance details Defined in Language.Hakaru.Types.Sing data Sing (a :: [[HakaruFun]]) where SVoid :: Sing ('[] :: [[HakaruFun]]) SPlus :: forall (xs :: [HakaruFun]) (xss :: [[HakaruFun]]). !(Sing xs) -> !(Sing xss) -> Sing (xs ': xss)
data Sing (a :: [HakaruFun]) Source #
Instance details Defined in Language.Hakaru.Types.Sing data Sing (a :: [HakaruFun]) where SDone :: Sing ('[] :: [HakaruFun]) SEt :: forall (x :: HakaruFun) (xs :: [HakaruFun]). !(Sing x) -> !(Sing xs) -> Sing (x ': xs)

class SingI (a :: k) where Source #

A class for automatically generating the singleton for a given Hakaru type.

Methods

sing :: Sing a Source #

Instances

Instances details

KnownSymbol s => SingI (s :: Symbol) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods sing :: Sing s Source #
SingI 'I Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods sing :: Sing 'I Source #
SingI 'HNat Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods sing :: Sing 'HNat Source #
SingI 'HInt Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods sing :: Sing 'HInt Source #
SingI 'HProb Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods sing :: Sing 'HProb Source #
SingI 'HReal Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods sing :: Sing 'HReal Source #
SingI 'U Source #
Instance details Defined in Language.Hakaru.Parser.AST Methods sing :: Sing 'U Source #
KnownSymbol s => SingI ('TyCon s :: HakaruCon) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods sing :: Sing ('TyCon s) Source #
SingI a => SingI ('K a :: HakaruFun) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods sing :: Sing ('K a) Source #
SingI a => SingI ('HMeasure a :: Hakaru) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods sing :: Sing ('HMeasure a) Source #
SingI a => SingI ('HArray a :: Hakaru) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods sing :: Sing ('HArray a) Source #
(SingI a, SingI b) => SingI (a :@ b :: HakaruCon) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods sing :: Sing (a :@ b) Source #
(SingI a, SingI b) => SingI (a :-> b :: Hakaru) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods sing :: Sing (a :-> b) Source #
(sop ~ Code t, SingI t, SingI sop) => SingI ('HData t sop :: Hakaru) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods sing :: Sing ('HData t sop) Source #
SingI ('[] :: [[HakaruFun]]) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods sing :: Sing '[] Source #
SingI ('[] :: [HakaruFun]) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods sing :: Sing '[] Source #
(SingI xs, SingI xss) => SingI (xs ': xss :: [[HakaruFun]]) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods sing :: Sing (xs ': xss) Source #
(SingI x, SingI xs) => SingI (x ': xs :: [HakaruFun]) Source #
Instance details Defined in Language.Hakaru.Types.Sing Methods sing :: Sing (x ': xs) Source #