Language.Hakaru.Types.Sing

Singleton types for the Hakaru kind, and a decision procedure for Hakaru type-equality.

Documentation

data family Sing (a :: k) :: * infixr 7 `SEt`infixr 6 `SPlus`infixr 0 `SFun`

The data families of singletons for each kind.

Instances

JmEq1 (Sing :: Symbol -> *)

Methods

jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)

JmEq1 (Sing :: HakaruCon -> *)

Methods

jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)

JmEq1 (Sing :: HakaruFun -> *)

Methods

jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)

JmEq1 (Sing :: Hakaru -> *)

Methods

jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)

JmEq1 (Sing :: Untyped -> *)

Methods

jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)

Eq1 (Sing :: Symbol -> *)

Methods

eq1 :: Sing i -> Sing i -> Bool

Eq1 (Sing :: HakaruCon -> *)

Methods

eq1 :: Sing i -> Sing i -> Bool

Eq1 (Sing :: HakaruFun -> *)

Methods

eq1 :: Sing i -> Sing i -> Bool

Eq1 (Sing :: Hakaru -> *)

Methods

eq1 :: Sing i -> Sing i -> Bool

Eq1 (Sing :: Untyped -> *)

Methods

eq1 :: Sing i -> Sing i -> Bool

Show1 (Sing :: Symbol -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

Show1 (Sing :: HakaruCon -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

Show1 (Sing :: HakaruFun -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

Show1 (Sing :: Hakaru -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

Show1 (Sing :: Untyped -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

Coerce (Sing :: Hakaru -> *)

Methods

coerceTo :: Coercion a b -> Sing a -> Sing b

coerceFrom :: Coercion a b -> Sing b -> Sing a

PrimCoerce (Sing :: Hakaru -> *)

Methods

primCoerceTo :: PrimCoercion a b -> Sing a -> Sing b

primCoerceFrom :: PrimCoercion a b -> Sing b -> Sing a

JmEq1 (Sing :: [[HakaruFun]] -> *)

Methods

jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)

JmEq1 (Sing :: [HakaruFun] -> *)

Methods

jmEq1 :: Sing i -> Sing j -> Maybe (TypeEq i j)

Eq1 (Sing :: [[HakaruFun]] -> *)

Methods

eq1 :: Sing i -> Sing i -> Bool

Eq1 (Sing :: [HakaruFun] -> *)

Methods

eq1 :: Sing i -> Sing i -> Bool

Show1 (Sing :: [[HakaruFun]] -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

Show1 (Sing :: [HakaruFun] -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

Eq (Sing a)

Methods

(==) :: Sing a -> Sing a -> Bool

(/=) :: Sing a -> Sing a -> Bool

Eq (Sing a)

Methods

(==) :: Sing a -> Sing a -> Bool

(/=) :: Sing a -> Sing a -> Bool

Eq (Sing s)

Methods

(==) :: Sing s -> Sing s -> Bool

(/=) :: Sing s -> Sing s -> Bool

Eq (Sing a)

Methods

(==) :: Sing a -> Sing a -> Bool

(/=) :: Sing a -> Sing a -> Bool

Eq (Sing a)

Methods

(==) :: Sing a -> Sing a -> Bool

(/=) :: Sing a -> Sing a -> Bool

Eq (Sing a)

Methods

(==) :: Sing a -> Sing a -> Bool

(/=) :: Sing a -> Sing a -> Bool

Eq (Sing a)

Methods

(==) :: Sing a -> Sing a -> Bool

(/=) :: Sing a -> Sing a -> Bool

Show (Sing a)

Methods

showsPrec :: Int -> Sing a -> ShowS

show :: Sing a -> String

showList :: [Sing a] -> ShowS

Show (Sing a)

Methods

showsPrec :: Int -> Sing a -> ShowS

show :: Sing a -> String

showList :: [Sing a] -> ShowS

Show (Sing s)

Methods

showsPrec :: Int -> Sing s -> ShowS

show :: Sing s -> String

showList :: [Sing s] -> ShowS

Show (Sing a)

Methods

showsPrec :: Int -> Sing a -> ShowS

show :: Sing a -> String

showList :: [Sing a] -> ShowS

Show (Sing a)

Methods

showsPrec :: Int -> Sing a -> ShowS

show :: Sing a -> String

showList :: [Sing a] -> ShowS

Show (Sing a)

Methods

showsPrec :: Int -> Sing a -> ShowS

show :: Sing a -> String

showList :: [Sing a] -> ShowS

Show (Sing a)

Methods

showsPrec :: Int -> Sing a -> ShowS

show :: Sing a -> String

showList :: [Sing a] -> ShowS

TCMTypeRepr (Sing x)

Methods

toTypeRepr :: Sing x -> Maybe (Either Text (Some1 Sing))

data Sing (s :: Symbol)

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).

data Sing (s :: Symbol) where

• SingSymbol :: Sing s

data Sing (a :: HakaruCon)

data Sing (a :: HakaruCon) where

• STyCon :: Sing (TyCon s)
• STyApp :: Sing (a :@ b)

data Sing (a :: HakaruFun)

data Sing (a :: HakaruFun) where

• SIdent :: Sing I
• SKonst :: Sing (K a)

data Sing (a :: Hakaru)

Singleton types for the kind of Hakaru types. We need to use this instead of Proxy in order to implement jmEq1.

data Sing (a :: Hakaru) where

• SNat :: Sing HNat
• SInt :: Sing HInt
• SProb :: Sing HProb
• SReal :: Sing HReal
• SMeasure :: Sing (HMeasure a)
• SArray :: Sing (HArray a)
• SFun :: Sing (a :-> b)
• SData :: Sing (HData' t)

data Sing (a :: Untyped)

data Sing (a :: Untyped) where

• SU :: Sing U

data Sing (a :: [[HakaruFun]])

data Sing (a :: [[HakaruFun]]) where

• SVoid :: Sing ([] :: [[HakaruFun]])
• SPlus :: Sing (xs ': xss)

data Sing (a :: [HakaruFun])

data Sing (a :: [HakaruFun]) where

• SDone :: Sing ([] :: [HakaruFun])
• SEt :: Sing (x ': xs)

class SingI (a :: k) where

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

Minimal complete definition

sing

Methods

sing :: Sing a

Instances

KnownSymbol s => SingI (s :: Symbol)

Methods

sing :: Sing s

SingI I

Methods

sing :: Sing I

SingI HNat

Methods

sing :: Sing HNat

SingI HInt

Methods

sing :: Sing HInt

SingI HProb

Methods

sing :: Sing HProb

SingI HReal

Methods

sing :: Sing HReal

SingI U

Methods

sing :: Sing U

KnownSymbol s => SingI (TyCon s :: HakaruCon)

Methods

sing :: Sing (TyCon s)

SingI a => SingI (K a :: HakaruFun)

Methods

sing :: Sing (K a)

SingI a => SingI (HMeasure a :: Hakaru)

Methods

sing :: Sing (HMeasure a)

SingI a => SingI (HArray a :: Hakaru)

Methods

sing :: Sing (HArray a)

(SingI a, SingI b) => SingI (a :@ b :: HakaruCon)

Methods

sing :: Sing (a :@ b)

(SingI a, SingI b) => SingI (a :-> b :: Hakaru)

Methods

sing :: Sing (a :-> b)

(sop ~ Code t, SingI t, SingI sop) => SingI (HData t sop :: Hakaru)

Methods

sing :: Sing (HData t sop)

SingI ([] :: [[HakaruFun]])

Methods

sing :: Sing []

SingI ([] :: [HakaruFun])

Methods

sing :: Sing []

(SingI xs, SingI xss) => SingI (xs ': xss :: [[HakaruFun]])

Methods

sing :: Sing (xs ': xss)

(SingI x, SingI xs) => SingI (x ': xs :: [HakaruFun])

Methods

sing :: Sing (x ': xs)

singOf :: SingI a => proxy a -> Sing a

Some helpful shorthands for "built-in" datatypes

Constructing singletons

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)

Destructing singletons

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)

Singletons for Symbol

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"