Language.Hakaru.Types.DataKind

A data-kind for the universe of Hakaru types.

The core definition of Hakaru types

data Hakaru

The universe/kind of Hakaru types.

Constructors

HNat

The natural numbers; aka, the non-negative integers.

HInt

The integers.

HProb

Non-negative real numbers. Unlike what you might expect, this is not restructed to the [0,1] interval!

HReal

The affinely extended real number line. That is, the real numbers extended with positive and negative infinities.

HMeasure !Hakaru

The measure monad

HArray !Hakaru

The built-in type for uniform arrays.

!Hakaru :-> !Hakaru infixr 0

The type of Hakaru functions.

HData !HakaruCon [[HakaruFun]]

A user-defined polynomial datatype. Each such type is specified by a "tag" (the HakaruCon) which names the type, and a sum-of-product representation of the type itself.

Instances

Category Coercion

Methods

id :: Coercion a a

(.) :: Coercion b c -> Coercion a b -> Coercion a c

JmEq1 HContinuous

Methods

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

JmEq1 HDiscrete

Methods

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

JmEq1 HIntegrable

Methods

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

JmEq1 HRadical

Methods

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

JmEq1 HFractional

Methods

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

JmEq1 HRing

Methods

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

JmEq1 HSemiring

Methods

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

JmEq1 NaryOp

Methods

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

JmEq1 Literal

Methods

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

Eq1 HContinuous

Methods

eq1 :: HContinuous i -> HContinuous i -> Bool

Eq1 HDiscrete

Methods

eq1 :: HDiscrete i -> HDiscrete i -> Bool

Eq1 HIntegrable

Methods

eq1 :: HIntegrable i -> HIntegrable i -> Bool

Eq1 HRadical

Methods

eq1 :: HRadical i -> HRadical i -> Bool

Eq1 HFractional

Methods

eq1 :: HFractional i -> HFractional i -> Bool

Eq1 HRing

Methods

eq1 :: HRing i -> HRing i -> Bool

Eq1 HSemiring

Methods

eq1 :: HSemiring i -> HSemiring i -> Bool

Eq1 Value

Methods

eq1 :: Value i -> Value i -> Bool

Eq1 NaryOp

Methods

eq1 :: NaryOp i -> NaryOp i -> Bool

Eq1 Literal

Methods

eq1 :: Literal i -> Literal i -> Bool

Show1 Value

Methods

showsPrec1 :: Int -> Value i -> ShowS

show1 :: Value i -> String

Show1 Literal

Methods

showsPrec1 :: Int -> Literal i -> ShowS

show1 :: Literal i -> String

SingI HNat

Methods

sing :: Sing HNat

SingI HInt

Methods

sing :: Sing HInt

SingI HProb

Methods

sing :: Sing HProb

SingI HReal

Methods

sing :: Sing HReal

Traversable11 Datum

Methods

traverse11 :: Applicative f => (forall (i :: k1). a i -> f (b i)) -> Datum a j -> f (Datum b j)

Foldable11 Datum

Methods

fold11 :: Monoid m => Datum (Lift1 m) i -> m

foldMap11 :: Monoid m => (forall (i :: k1). a i -> m) -> Datum a j -> m

Functor11 Datum

Methods

fmap11 :: (forall (i :: k1). a i -> b i) -> Datum a j -> Datum b j

JmEq2 PrimCoercion

Methods

jmEq2 :: PrimCoercion i1 j1 -> PrimCoercion i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)

Eq2 Coercion

Methods

eq2 :: Coercion i j -> Coercion i j -> Bool

Eq2 PrimCoercion

Methods

eq2 :: PrimCoercion i j -> PrimCoercion i j -> Bool

Traversable11 (DatumFun x :: (Hakaru -> *) -> Hakaru -> *)

Methods

traverse11 :: Applicative f => (forall (i :: k1). a i -> f (b i)) -> DatumFun x a j -> f (DatumFun x b j)

Traversable11 (DatumStruct xs :: (Hakaru -> *) -> Hakaru -> *)

Methods

traverse11 :: Applicative f => (forall (i :: k1). a i -> f (b i)) -> DatumStruct xs a j -> f (DatumStruct xs b j)

Traversable11 (DatumCode xss :: (Hakaru -> *) -> Hakaru -> *)

Methods

traverse11 :: Applicative f => (forall (i :: k1). a i -> f (b i)) -> DatumCode xss a j -> f (DatumCode xss b j)

Foldable11 (DatumFun x :: (Hakaru -> *) -> Hakaru -> *)

Methods

fold11 :: Monoid m => DatumFun x (Lift1 m) i -> m

foldMap11 :: Monoid m => (forall (i :: k1). a i -> m) -> DatumFun x a j -> m

Foldable11 (DatumStruct xs :: (Hakaru -> *) -> Hakaru -> *)

Methods

fold11 :: Monoid m => DatumStruct xs (Lift1 m) i -> m

foldMap11 :: Monoid m => (forall (i :: k1). a i -> m) -> DatumStruct xs a j -> m

Foldable11 (DatumCode xss :: (Hakaru -> *) -> Hakaru -> *)

Methods

fold11 :: Monoid m => DatumCode xss (Lift1 m) i -> m

foldMap11 :: Monoid m => (forall (i :: k1). a i -> m) -> DatumCode xss a j -> m

Functor11 (DatumFun x :: (Hakaru -> *) -> Hakaru -> *)

Methods

fmap11 :: (forall (i :: k1). a i -> b i) -> DatumFun x a j -> DatumFun x b j

Functor11 (DatumStruct xs :: (Hakaru -> *) -> Hakaru -> *)

Methods

fmap11 :: (forall (i :: k1). a i -> b i) -> DatumStruct xs a j -> DatumStruct xs b j

Functor11 (DatumCode xss :: (Hakaru -> *) -> Hakaru -> *)

Methods

fmap11 :: (forall (i :: k1). a i -> b i) -> DatumCode xss a j -> DatumCode xss b j

JmEq1 (Sing :: Hakaru -> *)

Methods

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

JmEq1 (PrimCoercion a :: Hakaru -> *)

Methods

jmEq1 :: PrimCoercion a i -> PrimCoercion a j -> Maybe (TypeEq i j)

Eq1 ast => JmEq1 (Datum ast :: Hakaru -> *)

Methods

jmEq1 :: Datum ast i -> Datum ast j -> Maybe (TypeEq i j)

(ABT Term abt, JmEq2 abt) => JmEq1 (Term abt :: Hakaru -> *)

Methods

jmEq1 :: Term abt i -> Term abt j -> Maybe (TypeEq i j)

Eq1 (Sing :: Hakaru -> *)

Methods

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

Eq1 (Coercion a :: Hakaru -> *)

Methods

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

Eq1 (PrimCoercion a :: Hakaru -> *)

Methods

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

Eq1 (Pattern vars :: Hakaru -> *)

Methods

eq1 :: Pattern vars i -> Pattern vars i -> Bool

Eq1 ast => Eq1 (Datum ast :: Hakaru -> *)

Methods

eq1 :: Datum ast i -> Datum ast i -> Bool

(ABT Term abt, JmEq2 abt) => Eq1 (Term abt :: Hakaru -> *)

Methods

eq1 :: Term abt i -> Term abt i -> Bool

Eq1 (MeasureOp typs :: Hakaru -> *)

Methods

eq1 :: MeasureOp typs i -> MeasureOp typs i -> Bool

Eq1 (ArrayOp args :: Hakaru -> *)

Methods

eq1 :: ArrayOp args i -> ArrayOp args i -> Bool

Eq1 (PrimOp args :: Hakaru -> *)

Methods

eq1 :: PrimOp args i -> PrimOp args i -> Bool

Show1 (Sing :: Hakaru -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

Show1 (Pattern vars :: Hakaru -> *)

Methods

showsPrec1 :: Int -> Pattern vars i -> ShowS

show1 :: Pattern vars i -> String

Show1 ast => Show1 (Datum ast :: Hakaru -> *)

Methods

showsPrec1 :: Int -> Datum ast i -> ShowS

show1 :: Datum ast i -> String

Show2 abt => Show1 (LC_ abt :: Hakaru -> *)

Methods

showsPrec1 :: Int -> LC_ abt i -> ShowS

show1 :: LC_ abt i -> String

Show2 abt => Show1 (Term abt :: Hakaru -> *)

Methods

showsPrec1 :: Int -> Term abt i -> ShowS

show1 :: Term abt i -> String

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

Methods

sing :: Sing (HMeasure a)

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

Methods

sing :: Sing (HArray a)

JmEq2 abt => JmEq1 (Reducer abt xs :: Hakaru -> *)

Methods

jmEq1 :: Reducer abt xs i -> Reducer abt xs j -> Maybe (TypeEq i j)

Eq2 abt => Eq1 (Reducer abt xs :: Hakaru -> *)

Methods

eq1 :: Reducer abt xs i -> Reducer abt xs i -> Bool

Eq2 abt => Eq1 (Branch a abt :: Hakaru -> *)

Methods

eq1 :: Branch a abt i -> Branch a abt i -> Bool

Eq1 (PDatumFun x vars :: Hakaru -> *)

Methods

eq1 :: PDatumFun x vars i -> PDatumFun x vars i -> Bool

Eq1 (PDatumStruct xs vars :: Hakaru -> *)

Methods

eq1 :: PDatumStruct xs vars i -> PDatumStruct xs vars i -> Bool

Eq1 (PDatumCode xss vars :: Hakaru -> *)

Methods

eq1 :: PDatumCode xss vars i -> PDatumCode xss vars i -> Bool

Eq1 ast => Eq1 (DatumFun x ast :: Hakaru -> *)

Methods

eq1 :: DatumFun x ast i -> DatumFun x ast i -> Bool

Eq1 ast => Eq1 (DatumStruct xs ast :: Hakaru -> *)

Methods

eq1 :: DatumStruct xs ast i -> DatumStruct xs ast i -> Bool

Eq1 ast => Eq1 (DatumCode xss ast :: Hakaru -> *)

Methods

eq1 :: DatumCode xss ast i -> DatumCode xss ast i -> Bool

Show2 abt => Show1 (Branch a abt :: Hakaru -> *)

Methods

showsPrec1 :: Int -> Branch a abt i -> ShowS

show1 :: Branch a abt i -> String

Show1 (PDatumFun x vars :: Hakaru -> *)

Methods

showsPrec1 :: Int -> PDatumFun x vars i -> ShowS

show1 :: PDatumFun x vars i -> String

Show1 (PDatumStruct xs vars :: Hakaru -> *)

Methods

showsPrec1 :: Int -> PDatumStruct xs vars i -> ShowS

show1 :: PDatumStruct xs vars i -> String

Show1 (PDatumCode xss vars :: Hakaru -> *)

Methods

showsPrec1 :: Int -> PDatumCode xss vars i -> ShowS

show1 :: PDatumCode xss vars i -> String

Show1 ast => Show1 (DatumFun x ast :: Hakaru -> *)

Methods

showsPrec1 :: Int -> DatumFun x ast i -> ShowS

show1 :: DatumFun x ast i -> String

Show1 ast => Show1 (DatumStruct xs ast :: Hakaru -> *)

Methods

showsPrec1 :: Int -> DatumStruct xs ast i -> ShowS

show1 :: DatumStruct xs ast i -> String

Show1 ast => Show1 (DatumCode xss ast :: Hakaru -> *)

Methods

showsPrec1 :: Int -> DatumCode xss ast i -> ShowS

show1 :: DatumCode xss ast i -> String

(Show1 ast, Show2 abt) => Show1 (MatchResult ast abt :: Hakaru -> *)

Methods

showsPrec1 :: Int -> MatchResult ast abt i -> ShowS

show1 :: MatchResult ast abt i -> String

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

ABT Term abt => Eq (Index (abt ([] :: [Hakaru])))

Methods

(==) :: Index (abt []) -> Index (abt []) -> Bool

(/=) :: Index (abt []) -> Index (abt []) -> Bool

ABT Term abt => Ord (Index (abt ([] :: [Hakaru])))

Methods

compare :: Index (abt []) -> Index (abt []) -> Ordering

(<) :: Index (abt []) -> Index (abt []) -> Bool

(<=) :: Index (abt []) -> Index (abt []) -> Bool

(>) :: Index (abt []) -> Index (abt []) -> Bool

(>=) :: Index (abt []) -> Index (abt []) -> Bool

max :: Index (abt []) -> Index (abt []) -> Index (abt [])

min :: Index (abt []) -> Index (abt []) -> Index (abt [])

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

JmEq2 MeasureOp

Methods

jmEq2 :: MeasureOp i1 j1 -> MeasureOp i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)

JmEq2 ArrayOp

Methods

jmEq2 :: ArrayOp i1 j1 -> ArrayOp i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)

JmEq2 PrimOp

Methods

jmEq2 :: PrimOp i1 j1 -> PrimOp i2 j2 -> Maybe (TypeEq i1 i2, TypeEq j1 j2)

Eq2 Pattern

Methods

eq2 :: Pattern i j -> Pattern i j -> Bool

Eq2 MeasureOp

Methods

eq2 :: MeasureOp i j -> MeasureOp i j -> Bool

Eq2 ArrayOp

Methods

eq2 :: ArrayOp i j -> ArrayOp i j -> Bool

Eq2 PrimOp

Methods

eq2 :: PrimOp i j -> PrimOp i j -> Bool

Show2 Pattern

Methods

showsPrec2 :: Int -> Pattern i j -> ShowS

show2 :: Pattern i j -> String

Traversable21 Term

Methods

traverse21 :: Applicative f => (forall (h :: k1) (i :: k2). a h i -> f (b h i)) -> Term a j -> f (Term b j)

Traversable21 Head

Methods

traverse21 :: Applicative f => (forall (h :: k1) (i :: k2). a h i -> f (b h i)) -> Head a j -> f (Head b j)

Foldable21 Term

Methods

fold21 :: Monoid m => Term (Lift2 m) j -> m

foldMap21 :: Monoid m => (forall (h :: k1) (i :: k2). a h i -> m) -> Term a j -> m

Foldable21 Head

Methods

fold21 :: Monoid m => Head (Lift2 m) j -> m

foldMap21 :: Monoid m => (forall (h :: k1) (i :: k2). a h i -> m) -> Head a j -> m

Functor21 Term

Methods

fmap21 :: (forall (h :: k1) (i :: k2). a h i -> b h i) -> Term a j -> Term b j

Functor21 Head

Methods

fmap21 :: (forall (h :: k1) (i :: k2). a h i -> b h i) -> Head a j -> Head b j

Traversable21 (Branch a :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> *)

Methods

traverse21 :: Applicative f => (forall (h :: k1) (i :: k2). a0 h i -> f (b h i)) -> Branch a a0 j -> f (Branch a b j)

Foldable21 (Branch a :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> *)

Methods

fold21 :: Monoid m => Branch a (Lift2 m) j -> m

foldMap21 :: Monoid m => (forall (h :: k1) (i :: k2). a0 h i -> m) -> Branch a a0 j -> m

Functor21 (Branch a :: ([Hakaru] -> Hakaru -> *) -> Hakaru -> *)

Methods

fmap21 :: (forall (h :: k1) (i :: k2). a0 h i -> b h i) -> Branch a a0 j -> Branch a b j

Eq2 (PDatumFun x :: [Hakaru] -> Hakaru -> *)

Methods

eq2 :: PDatumFun x i j -> PDatumFun x i j -> Bool

Eq2 (PDatumStruct xs :: [Hakaru] -> Hakaru -> *)

Methods

eq2 :: PDatumStruct xs i j -> PDatumStruct xs i j -> Bool

Eq2 (PDatumCode xss :: [Hakaru] -> Hakaru -> *)

Methods

eq2 :: PDatumCode xss i j -> PDatumCode xss i j -> Bool

Show2 (PDatumFun x :: [Hakaru] -> Hakaru -> *)

Methods

showsPrec2 :: Int -> PDatumFun x i j -> ShowS

show2 :: PDatumFun x i j -> String

Show2 (PDatumStruct xs :: [Hakaru] -> Hakaru -> *)

Methods

showsPrec2 :: Int -> PDatumStruct xs i j -> ShowS

show2 :: PDatumStruct xs i j -> String

Show2 (PDatumCode xss :: [Hakaru] -> Hakaru -> *)

Methods

showsPrec2 :: Int -> PDatumCode xss i j -> ShowS

show2 :: PDatumCode xss i j -> String

Traversable21 SArgs

Methods

traverse21 :: Applicative f => (forall (h :: k1) (i :: k2). a h i -> f (b h i)) -> SArgs a j -> f (SArgs b j)

Foldable21 SArgs

Methods

fold21 :: Monoid m => SArgs (Lift2 m) j -> m

foldMap21 :: Monoid m => (forall (h :: k1) (i :: k2). a h i -> m) -> SArgs a j -> m

Functor21 SArgs

Methods

fmap21 :: (forall (h :: k1) (i :: k2). a h i -> b h i) -> SArgs a j -> SArgs b j

Traversable22 Reducer

Methods

traverse22 :: Applicative f => (forall (h :: k1) (i :: k2). a h i -> f (b h i)) -> Reducer a j l -> f (Reducer b j l)

Foldable22 Reducer

Methods

fold22 :: Monoid m => Reducer (Lift2 m) j l -> m

foldMap22 :: Monoid m => (forall (h :: k1) (i :: k2). a h i -> m) -> Reducer a j l -> m

Functor22 Reducer

Methods

fmap22 :: (forall (h :: k1) (i :: k2). a h i -> b h i) -> Reducer a j l -> Reducer b j l

JmEq2 abt => JmEq1 (SArgs abt :: [([Hakaru], Hakaru)] -> *)

Methods

jmEq1 :: SArgs abt i -> SArgs abt j -> Maybe (TypeEq i j)

Eq2 abt => Eq1 (SArgs abt :: [([Hakaru], Hakaru)] -> *)

Methods

eq1 :: SArgs abt i -> SArgs abt i -> Bool

Show2 abt => Show1 (SArgs abt :: [([Hakaru], Hakaru)] -> *)

Methods

showsPrec1 :: Int -> SArgs abt i -> ShowS

show1 :: SArgs abt i -> String

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

HasTransformCtx (Variable a)

Methods

ctxOf :: Variable a -> TransformCtx

TCMTypeRepr (Sing x)

Methods

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

Eq (Some2 Transform)

Methods

(==) :: Some2 Transform -> Some2 Transform -> Bool

(/=) :: Some2 Transform -> Some2 Transform -> Bool

Read (Some2 Transform)

Methods

readsPrec :: Int -> ReadS (Some2 Transform)

readList :: ReadS [Some2 Transform]

readPrec :: ReadPrec (Some2 Transform)

readListPrec :: ReadPrec [Some2 Transform]

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 HakaruFun

The identity and constant functors on Hakaru. This gives us limited access to type-variables in Hakaru, for use in recursive sums-of-products. Notably, however, it only allows a single variable (namely the one bound by the closest binder) so it can't encode mutual recursion or other non-local uses of multiple binders. We also cannot encode non-regular recursive types (aka nested datatypes), like rose trees. To do that, we'd need to allow any old functor here.

Products and sums are represented as lists in the Hakaru data-kind itself, so they aren't in this datatype.

Constructors

I

K !Hakaru

Instances

HOrd_ HUnit

Methods

hOrd :: HOrd HUnit

HOrd_ HBool

Methods

hOrd :: HOrd HBool

HEq_ HUnit

Methods

hEq :: HEq HUnit

HEq_ HBool

Methods

hEq :: HEq HBool

SingI I

Methods

sing :: Sing I

Interp HUnit ()

Methods

reify :: ABT Term abt => Head abt HUnit -> ()

reflect :: ABT Term abt => () -> Head abt HUnit

Interp HBool Bool

Methods

reify :: ABT Term abt => Head abt HBool -> Bool

reflect :: ABT Term abt => Bool -> Head abt HBool

JmEq1 (Sing :: HakaruFun -> *)

Methods

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

Eq1 (Sing :: HakaruFun -> *)

Methods

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

Show1 (Sing :: HakaruFun -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

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

Methods

sing :: Sing (K 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

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)

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

Methods

showsPrec :: Int -> Sing a -> ShowS

show :: Sing a -> String

showList :: [Sing a] -> ShowS

(HOrd_ a, HOrd_ b) => HOrd_ (HEither a b)

Methods

hOrd :: HOrd (HEither a b)

(HOrd_ a, HOrd_ b) => HOrd_ (HPair a b)

Methods

hOrd :: HOrd (HPair a b)

(HEq_ a, HEq_ b) => HEq_ (HEither a b)

Methods

hEq :: HEq (HEither a b)

(HEq_ a, HEq_ b) => HEq_ (HPair a b)

Methods

hEq :: HEq (HPair a b)

data Sing (a :: HakaruFun)

data Sing (a :: HakaruFun) where

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

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)

data HakaruCon

The kind of user-defined Hakaru type constructors, which serves as a tag for the sum-of-products representation of the user-defined Hakaru type. The head of the HakaruCon is a symbolic name, and the rest are arguments to that type constructor. The a parameter is parametric, which is especially useful when you need a singleton of the constructor. The argument positions are necessary to do variable binding in Code. Symbol is the kind of "type level strings".

Constructors

TyCon !Symbol

HakaruCon :@ Hakaru infixl 0

Instances

JmEq1 (Sing :: HakaruCon -> *)

Methods

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

Eq1 (Sing :: HakaruCon -> *)

Methods

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

Show1 (Sing :: HakaruCon -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

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

Methods

sing :: Sing (TyCon s)

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

Methods

sing :: Sing (a :@ b)

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

data Sing (a :: HakaruCon)

data Sing (a :: HakaruCon) where

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

data Symbol

(Kind) This is the kind of type-level symbols. Declared here because class IP needs it

Instances

SingKind Symbol

Since: 4.9.0.0

Associated Types

type DemoteRep Symbol :: *

Methods

fromSing :: Sing a -> DemoteRep Symbol

KnownSymbol a => SingI (a :: Symbol)

Since: 4.9.0.0

Methods

sing :: Sing a

KnownSymbol s => SingI (s :: Symbol)

Methods

sing :: Sing s

JmEq1 (Sing :: Symbol -> *)

Methods

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

Eq1 (Sing :: Symbol -> *)

Methods

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

Show1 (Sing :: Symbol -> *)

Methods

showsPrec1 :: Int -> Sing i -> ShowS

show1 :: Sing i -> String

Eq (Sing s)

Methods

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

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

Show (Sing s)

Methods

showsPrec :: Int -> Sing s -> ShowS

show :: Sing s -> String

showList :: [Sing s] -> ShowS

data Sing (s :: Symbol)

data Sing (s :: Symbol) where

• SSym :: Sing s

type DemoteRep Symbol

type DemoteRep Symbol = String

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

type family Code (a :: HakaruCon) :: [[HakaruFun]]

The Code type family allows users to extend the Hakaru language by adding new types. The right hand side is the sum-of-products representation of that type. See the "built-in" types for examples.

Instances

type Code (TyCon "Bool")

type Code (TyCon "Bool") = ([] :: [HakaruFun]) ': (([] :: [HakaruFun]) ': ([] :: [[HakaruFun]]))

type Code (TyCon "Unit")

type Code (TyCon "Unit") = ([] :: [HakaruFun]) ': ([] :: [[HakaruFun]])

type Code (TyCon "List" :@ a)

type Code (TyCon "List" :@ a) = ([] :: [HakaruFun]) ': ((K a ': (I ': ([] :: [HakaruFun]))) ': ([] :: [[HakaruFun]]))

type Code (TyCon "Maybe" :@ a)

type Code (TyCon "Maybe" :@ a) = ([] :: [HakaruFun]) ': ((K a ': ([] :: [HakaruFun])) ': ([] :: [[HakaruFun]]))

type Code ((TyCon "Either" :@ a) :@ b)

type Code ((TyCon "Either" :@ a) :@ b) = (K a ': ([] :: [HakaruFun])) ': ((K b ': ([] :: [HakaruFun])) ': ([] :: [[HakaruFun]]))

type Code ((TyCon "Pair" :@ a) :@ b)

type Code ((TyCon "Pair" :@ a) :@ b) = (K a ': (K b ': ([] :: [HakaruFun]))) ': ([] :: [[HakaruFun]])

type HData' t = HData t (Code t)

A helper type alias for simplifying type signatures for user-provided Hakaru types.

BUG: you cannot use this alias when defining other type aliases! For some reason the type checker doesn't reduce the type family applications, which prevents the use of these type synonyms in class instance heads. Any type synonym created with HData' will suffer the same issue, so type synonyms must be written out by hand— or copied from the GHC pretty printer, which will happily reduce things in the repl, even in the presence of quantified type variables.

Some "built-in" types

type HBool = HData (TyCon "Bool") '['[], '[]]

type HUnit = HData (TyCon "Unit") '['[]]

type HPair a b = HData ((TyCon "Pair" :@ a) :@ b) '['[K a, K b]]

type HEither a b = HData ((TyCon "Either" :@ a) :@ b) '['[K a], '[K b]]

type HList a = HData (TyCon "List" :@ a) '['[], '[K a, I]]

type HMaybe a = HData (TyCon "Maybe" :@ a) '['[], '[K a]]