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 Hakaru Coercion

Methods

id :: cat a a

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

JmEq1 Hakaru HContinuous

Methods

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

JmEq1 Hakaru HDiscrete

Methods

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

JmEq1 Hakaru HIntegrable

Methods

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

JmEq1 Hakaru HRadical

Methods

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

JmEq1 Hakaru HFractional

Methods

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

JmEq1 Hakaru HRing

Methods

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

JmEq1 Hakaru HSemiring

Methods

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

JmEq1 Hakaru NaryOp

Methods

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

JmEq1 Hakaru Literal

Methods

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

Eq1 Hakaru HContinuous

Methods

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

Eq1 Hakaru HDiscrete

Methods

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

Eq1 Hakaru HIntegrable

Methods

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

Eq1 Hakaru HRadical

Methods

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

Eq1 Hakaru HFractional

Methods

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

Eq1 Hakaru HRing

Methods

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

Eq1 Hakaru HSemiring

Methods

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

Eq1 Hakaru NaryOp

Methods

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

Eq1 Hakaru Literal

Methods

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

Eq1 Hakaru Value

Methods

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

Show1 Hakaru Literal

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Show1 Hakaru Value

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

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

Traversable11 Hakaru Hakaru Datum

Methods

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

Foldable11 Hakaru Hakaru Datum

Methods

fold11 :: Monoid m => f (Lift1 k1 m) i -> m

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

Functor11 Hakaru Hakaru Datum

Methods

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

JmEq2 Hakaru Hakaru PrimCoercion

Methods

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

Eq2 Hakaru Hakaru Coercion

Methods

eq2 :: a i j -> a i j -> Bool

Eq2 Hakaru Hakaru PrimCoercion

Methods

eq2 :: a i j -> a i j -> Bool

Traversable11 Hakaru Hakaru (DatumFun x)

Methods

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

Traversable11 Hakaru Hakaru (DatumStruct xs)

Methods

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

Traversable11 Hakaru Hakaru (DatumCode xss)

Methods

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

Foldable11 Hakaru Hakaru (DatumFun x)

Methods

fold11 :: Monoid m => f (Lift1 k1 m) i -> m

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

Foldable11 Hakaru Hakaru (DatumStruct xs)

Methods

fold11 :: Monoid m => f (Lift1 k1 m) i -> m

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

Foldable11 Hakaru Hakaru (DatumCode xss)

Methods

fold11 :: Monoid m => f (Lift1 k1 m) i -> m

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

Functor11 Hakaru Hakaru (DatumFun x)

Methods

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

Functor11 Hakaru Hakaru (DatumStruct xs)

Methods

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

Functor11 Hakaru Hakaru (DatumCode xss)

Methods

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

Traversable21 Hakaru Hakaru [Hakaru] Term

Methods

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

Traversable21 Hakaru Hakaru [Hakaru] Head

Methods

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

Foldable21 Hakaru Hakaru [Hakaru] Term

Methods

fold21 :: Monoid m => f (Lift2 k2 k1 m) j -> m

foldMap21 :: Monoid m => (forall h i. a h i -> m) -> f a j -> m

Foldable21 Hakaru Hakaru [Hakaru] Head

Methods

fold21 :: Monoid m => f (Lift2 k2 k1 m) j -> m

foldMap21 :: Monoid m => (forall h i. a h i -> m) -> f a j -> m

Functor21 Hakaru Hakaru [Hakaru] Term

Methods

fmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j

Functor21 Hakaru Hakaru [Hakaru] Head

Methods

fmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j

Traversable21 Hakaru Hakaru [Hakaru] (Branch a)

Methods

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

Foldable21 Hakaru Hakaru [Hakaru] (Branch a)

Methods

fold21 :: Monoid m => f (Lift2 k2 k1 m) j -> m

foldMap21 :: Monoid m => (forall h i. a h i -> m) -> f a j -> m

Functor21 Hakaru Hakaru [Hakaru] (Branch a)

Methods

fmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j

JmEq1 Hakaru (Sing Hakaru)

Methods

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

JmEq1 Hakaru (PrimCoercion a)

Methods

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

Eq1 Hakaru ast => JmEq1 Hakaru (Datum ast)

Methods

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

Eq1 Hakaru (Sing Hakaru)

Methods

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

Eq1 Hakaru (Coercion a)

Methods

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

Eq1 Hakaru (PrimCoercion a)

Methods

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

Eq1 Hakaru (Pattern vars)

Methods

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

Eq1 Hakaru ast => Eq1 Hakaru (Datum ast)

Methods

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

Eq1 Hakaru (MeasureOp typs)

Methods

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

Eq1 Hakaru (ArrayOp args)

Methods

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

Eq1 Hakaru (PrimOp args)

Methods

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

Show1 Hakaru (Sing Hakaru)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Show1 Hakaru (Pattern vars)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Show1 Hakaru ast => Show1 Hakaru (Datum ast)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Show2 Hakaru [Hakaru] abt => Show1 Hakaru (LC_ abt)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Show2 Hakaru [Hakaru] abt => Show1 Hakaru (Term abt)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

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

JmEq2 Hakaru [Hakaru] MeasureOp

Methods

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

JmEq2 Hakaru [Hakaru] ArrayOp

Methods

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

JmEq2 Hakaru [Hakaru] PrimOp

Methods

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

Eq2 Hakaru [Hakaru] Pattern

Methods

eq2 :: a i j -> a i j -> Bool

Eq2 Hakaru [Hakaru] MeasureOp

Methods

eq2 :: a i j -> a i j -> Bool

Eq2 Hakaru [Hakaru] ArrayOp

Methods

eq2 :: a i j -> a i j -> Bool

Eq2 Hakaru [Hakaru] PrimOp

Methods

eq2 :: a i j -> a i j -> Bool

Show2 Hakaru [Hakaru] Pattern

Methods

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

show2 :: a i j -> String

Traversable22 Hakaru [Hakaru] Hakaru [Hakaru] Reducer

Methods

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

Foldable22 Hakaru [Hakaru] Hakaru [Hakaru] Reducer

Methods

fold22 :: Monoid m => f (Lift2 k2 k1 m) j l -> m

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

Functor22 Hakaru [Hakaru] Hakaru [Hakaru] Reducer

Methods

fmap22 :: (forall h i. a h i -> b h i) -> f a j l -> f b j l

Eq2 Hakaru [Hakaru] (PDatumFun x)

Methods

eq2 :: a i j -> a i j -> Bool

Eq2 Hakaru [Hakaru] (PDatumStruct xs)

Methods

eq2 :: a i j -> a i j -> Bool

Eq2 Hakaru [Hakaru] (PDatumCode xss)

Methods

eq2 :: a i j -> a i j -> Bool

Show2 Hakaru [Hakaru] (PDatumFun x)

Methods

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

show2 :: a i j -> String

Show2 Hakaru [Hakaru] (PDatumStruct xs)

Methods

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

show2 :: a i j -> String

Show2 Hakaru [Hakaru] (PDatumCode xss)

Methods

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

show2 :: a i j -> String

JmEq2 Hakaru [Hakaru] abt => JmEq1 Hakaru (Reducer abt xs)

Methods

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

Eq2 Hakaru [Hakaru] abt => Eq1 Hakaru (Reducer abt xs)

Methods

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

Eq2 Hakaru [Hakaru] abt => Eq1 Hakaru (Branch a abt)

Methods

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

Eq1 Hakaru (PDatumFun x vars)

Methods

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

Eq1 Hakaru (PDatumStruct xs vars)

Methods

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

Eq1 Hakaru (PDatumCode xss vars)

Methods

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

Eq1 Hakaru ast => Eq1 Hakaru (DatumFun x ast)

Methods

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

Eq1 Hakaru ast => Eq1 Hakaru (DatumStruct xs ast)

Methods

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

Eq1 Hakaru ast => Eq1 Hakaru (DatumCode xss ast)

Methods

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

Show2 Hakaru [Hakaru] abt => Show1 Hakaru (Branch a abt)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Show1 Hakaru (PDatumFun x vars)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Show1 Hakaru (PDatumStruct xs vars)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Show1 Hakaru (PDatumCode xss vars)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Show1 Hakaru ast => Show1 Hakaru (DatumFun x ast)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Show1 Hakaru ast => Show1 Hakaru (DatumStruct xs ast)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Show1 Hakaru ast => Show1 Hakaru (DatumCode xss ast)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

(Show1 Hakaru ast, Show2 Hakaru [Hakaru] abt) => Show1 Hakaru (MatchResult ast abt)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

(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

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

Methods

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

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

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

Methods

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

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

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

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

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

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

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

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

Traversable21 [([Hakaru], Hakaru)] Hakaru [Hakaru] SArgs

Methods

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

Foldable21 [([Hakaru], Hakaru)] Hakaru [Hakaru] SArgs

Methods

fold21 :: Monoid m => f (Lift2 k2 k1 m) j -> m

foldMap21 :: Monoid m => (forall h i. a h i -> m) -> f a j -> m

Functor21 [([Hakaru], Hakaru)] Hakaru [Hakaru] SArgs

Methods

fmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j

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

Methods

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

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

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Eq (Sing Hakaru a)

Methods

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

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

Show (Sing Hakaru a)

Methods

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

show :: Sing Hakaru a -> String

showList :: [Sing Hakaru a] -> ShowS

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 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 HakaruFun I

Methods

sing :: Sing I a

Interp HUnit ()

Methods

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

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

Interp HBool Bool

Methods

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

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

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

Show1 HakaruFun (Sing HakaruFun)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

SingI Hakaru a => SingI HakaruFun (K a)

Methods

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

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

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

Methods

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

(/=) :: Sing HakaruFun a -> Sing HakaruFun 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 HakaruFun a)

Methods

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

show :: Sing HakaruFun a -> String

showList :: [Sing HakaruFun 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 HakaruFun

data Sing HakaruFun where

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

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)

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

Methods

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

Eq1 HakaruCon (Sing HakaruCon)

Methods

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

Show1 HakaruCon (Sing HakaruCon)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

KnownSymbol s => SingI HakaruCon (TyCon s)

Methods

sing :: Sing (TyCon s) a

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

Methods

sing :: Sing (a :@ b) a

Eq (Sing HakaruCon a)

Methods

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

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

Show (Sing HakaruCon a)

Methods

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

show :: Sing HakaruCon a -> String

showList :: [Sing HakaruCon a] -> ShowS

data Sing HakaruCon

data Sing HakaruCon where

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

data Symbol :: *

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

Instances

KnownSymbol a => SingI Symbol a

Methods

sing :: Sing a a

KnownSymbol s => SingI Symbol s

Methods

sing :: Sing s a

SingKind Symbol (KProxy Symbol)

Associated Types

type DemoteRep (KProxy Symbol) (kparam :: KProxy (KProxy Symbol)) :: *

Methods

fromSing :: Sing (KProxy Symbol) a -> DemoteRep (KProxy Symbol) kparam

JmEq1 Symbol (Sing Symbol)

Methods

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

Eq1 Symbol (Sing Symbol)

Methods

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

Show1 Symbol (Sing Symbol)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Eq (Sing Symbol s)

Methods

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

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

Show (Sing Symbol s)

Methods

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

show :: Sing Symbol s -> String

showList :: [Sing Symbol s] -> ShowS

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol s

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

type (==) Symbol a b

type (==) Symbol a b = EqSymbol a b

type DemoteRep Symbol (KProxy Symbol)

type DemoteRep Symbol (KProxy Symbol) = String

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] ([] HakaruFun) ([] [HakaruFun]))

type Code (TyCon "Unit")

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

type Code ((:@) (TyCon "List") a)

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

type Code ((:@) (TyCon "Maybe") a)

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

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

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

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

type Code ((:@) ((:@) (TyCon "Pair") a) b) = (:) [HakaruFun] ((:) HakaruFun (K a) ((:) HakaruFun (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]]