Language.Hakaru.Types.Sing

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

Documentation

data family Sing (a :: k) :: *

The data families of singletons for each kind.

Instances

JmEq1 Symbol (Sing Symbol)

Methods

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

JmEq1 HakaruCon (Sing HakaruCon)

Methods

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

JmEq1 HakaruFun (Sing HakaruFun)

Methods

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

JmEq1 Hakaru (Sing Hakaru)

Methods

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

JmEq1 Untyped (Sing Untyped)

Methods

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

Eq1 Symbol (Sing Symbol)

Methods

eq1 :: a i -> a i -> Bool

Eq1 HakaruCon (Sing HakaruCon)

Methods

eq1 :: a i -> a i -> Bool

Eq1 HakaruFun (Sing HakaruFun)

Methods

eq1 :: a i -> a i -> Bool

Eq1 Hakaru (Sing Hakaru)

Methods

eq1 :: a i -> a i -> Bool

Eq1 Untyped (Sing Untyped)

Methods

eq1 :: a i -> a i -> Bool

Show1 Symbol (Sing Symbol)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Show1 HakaruCon (Sing HakaruCon)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Show1 HakaruFun (Sing HakaruFun)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Show1 Hakaru (Sing Hakaru)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Show1 Untyped (Sing Untyped)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Coerce (Sing Hakaru)

Methods

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

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

PrimCoerce (Sing Hakaru)

Methods

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

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

JmEq1 [[HakaruFun]] (Sing [[HakaruFun]])

Methods

jmEq1 :: a i -> a j -> Maybe (TypeEq (Sing [[HakaruFun]]) i j)

JmEq1 [HakaruFun] (Sing [HakaruFun])

Methods

jmEq1 :: a i -> a j -> Maybe (TypeEq (Sing [HakaruFun]) i j)

Eq1 [[HakaruFun]] (Sing [[HakaruFun]])

Methods

eq1 :: a i -> a i -> Bool

Eq1 [HakaruFun] (Sing [HakaruFun])

Methods

eq1 :: a i -> a i -> Bool

Show1 [[HakaruFun]] (Sing [[HakaruFun]])

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Show1 [HakaruFun] (Sing [HakaruFun])

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Eq (Sing [[HakaruFun]] a)

Methods

(==) :: Sing [[HakaruFun]] a -> Sing [[HakaruFun]] a -> Bool

(/=) :: Sing [[HakaruFun]] a -> Sing [[HakaruFun]] a -> Bool

Eq (Sing [HakaruFun] a)

Methods

(==) :: Sing [HakaruFun] a -> Sing [HakaruFun] a -> Bool

(/=) :: Sing [HakaruFun] a -> Sing [HakaruFun] a -> Bool

Eq (Sing Symbol s)

Methods

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

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

Eq (Sing HakaruCon a)

Methods

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

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

Eq (Sing HakaruFun a)

Methods

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

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

Eq (Sing Hakaru a)

Methods

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

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

Eq (Sing Untyped a)

Methods

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

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

Show (Sing [[HakaruFun]] a)

Methods

showsPrec :: Int -> Sing [[HakaruFun]] a -> ShowS

show :: Sing [[HakaruFun]] a -> String

showList :: [Sing [[HakaruFun]] a] -> ShowS

Show (Sing [HakaruFun] a)

Methods

showsPrec :: Int -> Sing [HakaruFun] a -> ShowS

show :: Sing [HakaruFun] a -> String

showList :: [Sing [HakaruFun] a] -> ShowS

Show (Sing Symbol s)

Methods

showsPrec :: Int -> Sing Symbol s -> ShowS

show :: Sing Symbol s -> String

showList :: [Sing Symbol s] -> ShowS

Show (Sing HakaruCon a)

Methods

showsPrec :: Int -> Sing HakaruCon a -> ShowS

show :: Sing HakaruCon a -> String

showList :: [Sing HakaruCon a] -> ShowS

Show (Sing HakaruFun a)

Methods

showsPrec :: Int -> Sing HakaruFun a -> ShowS

show :: Sing HakaruFun a -> String

showList :: [Sing HakaruFun a] -> ShowS

Show (Sing Hakaru a)

Methods

showsPrec :: Int -> Sing Hakaru a -> ShowS

show :: Sing Hakaru a -> String

showList :: [Sing Hakaru a] -> ShowS

Show (Sing Untyped a)

Methods

showsPrec :: Int -> Sing Untyped a -> ShowS

show :: Sing Untyped a -> String

showList :: [Sing Untyped a] -> ShowS

data Sing 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 Symbol where

• SingSymbol :: Sing Symbol s

data Sing HakaruCon

data Sing HakaruCon where

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

data Sing HakaruFun

data Sing HakaruFun where

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

data Sing Hakaru

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

data Sing Hakaru where

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

data Sing Untyped

data Sing Untyped where

• SU :: Sing Untyped U

data Sing [[HakaruFun]]

data Sing [[HakaruFun]] where

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

data Sing [HakaruFun]

data Sing [HakaruFun] where

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

class SingI a 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 Symbol s

Methods

sing :: Sing s a

SingI HakaruFun I

Methods

sing :: Sing I a

SingI Hakaru HNat

Methods

sing :: Sing HNat a

SingI Hakaru HInt

Methods

sing :: Sing HInt a

SingI Hakaru HProb

Methods

sing :: Sing HProb a

SingI Hakaru HReal

Methods

sing :: Sing HReal a

SingI Untyped U

Methods

sing :: Sing U a

KnownSymbol s => SingI HakaruCon (TyCon s)

Methods

sing :: Sing (TyCon s) a

SingI Hakaru a => SingI HakaruFun (K a)

Methods

sing :: Sing (K a) a

SingI Hakaru a => SingI Hakaru (HMeasure a)

Methods

sing :: Sing (HMeasure a) a

SingI Hakaru a => SingI Hakaru (HArray a)

Methods

sing :: Sing (HArray a) a

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

Methods

sing :: Sing (a :@ b) a

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

Methods

sing :: Sing (a :-> b) a

((~) [[HakaruFun]] sop (Code t), SingI HakaruCon t, SingI [[HakaruFun]] sop) => SingI Hakaru (HData t sop)

Methods

sing :: Sing (HData t sop) a

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

Methods

sing :: Sing [[HakaruFun]] a

SingI [HakaruFun] ([] HakaruFun)

Methods

sing :: Sing [HakaruFun] a

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

Methods

sing :: Sing (([HakaruFun] ': xs) xss) a

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

Methods

sing :: Sing ((HakaruFun ': x) xs) 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)

sUnEither :: Sing (HEither a b) -> (Sing a, Sing b)

sUnList :: Sing (HList a) -> Sing a

sUnMaybe :: Sing (HMaybe a) -> Sing a

Singletons for Symbol

sSymbol_Bool :: Sing "Bool"

sSymbol_Unit :: Sing "Unit"

sSymbol_Pair :: Sing "Pair"

sSymbol_Either :: Sing "Either"

sSymbol_List :: Sing "List"

sSymbol_Maybe :: Sing "Maybe"