hakaru-0.3.0: A probabilistic programming language

CopyrightCopyright (c) 2016 the Hakaru team
LicenseBSD3
Maintainerwren@community.haskell.org
Stabilityexperimental
PortabilityGHC-only
Safe HaskellSafe
LanguageHaskell2010

Language.Hakaru.Types.DataKind

Contents

Description

A data-kind for the universe of Hakaru types.

Synopsis

The core definition of Hakaru types

data Hakaru Source #

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 Source # 

Methods

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

JmEq1 Hakaru HDiscrete Source # 

Methods

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

JmEq1 Hakaru HIntegrable Source # 

Methods

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

JmEq1 Hakaru HRadical Source # 

Methods

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

JmEq1 Hakaru HFractional Source # 

Methods

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

JmEq1 Hakaru HRing Source # 

Methods

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

JmEq1 Hakaru HSemiring Source # 

Methods

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

JmEq1 Hakaru NaryOp Source # 

Methods

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

JmEq1 Hakaru Literal Source # 

Methods

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

Eq1 Hakaru HContinuous Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru HDiscrete Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru HIntegrable Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru HRadical Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru HFractional Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru HRing Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru HSemiring Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru NaryOp Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru Literal Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru Value Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Show1 Hakaru Literal Source # 

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

Show1 Hakaru Value Source # 

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

SingI Hakaru HNat Source # 

Methods

sing :: Sing HNat a Source #

SingI Hakaru HInt Source # 

Methods

sing :: Sing HInt a Source #

SingI Hakaru HProb Source # 

Methods

sing :: Sing HProb a Source #

SingI Hakaru HReal Source # 

Methods

sing :: Sing HReal a Source #

Traversable11 Hakaru Hakaru Datum Source # 

Methods

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

Foldable11 Hakaru Hakaru Datum Source # 

Methods

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

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

Functor11 Hakaru Hakaru Datum Source # 

Methods

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

JmEq2 Hakaru Hakaru PrimCoercion Source # 

Methods

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

Eq2 Hakaru Hakaru Coercion Source # 

Methods

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

Eq2 Hakaru Hakaru PrimCoercion Source # 

Methods

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

Traversable11 Hakaru Hakaru (DatumFun x) Source # 

Methods

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

Traversable11 Hakaru Hakaru (DatumStruct xs) Source # 

Methods

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

Traversable11 Hakaru Hakaru (DatumCode xss) Source # 

Methods

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

Foldable11 Hakaru Hakaru (DatumFun x) Source # 

Methods

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

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

Foldable11 Hakaru Hakaru (DatumStruct xs) Source # 

Methods

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

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

Foldable11 Hakaru Hakaru (DatumCode xss) Source # 

Methods

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

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

Functor11 Hakaru Hakaru (DatumFun x) Source # 

Methods

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

Functor11 Hakaru Hakaru (DatumStruct xs) Source # 

Methods

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

Functor11 Hakaru Hakaru (DatumCode xss) Source # 

Methods

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

Traversable21 Hakaru Hakaru [Hakaru] Term Source # 

Methods

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

Traversable21 Hakaru Hakaru [Hakaru] Lazy Source # 

Methods

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

Traversable21 Hakaru Hakaru [Hakaru] Whnf Source # 

Methods

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

Traversable21 Hakaru Hakaru [Hakaru] Head Source # 

Methods

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

Foldable21 Hakaru Hakaru [Hakaru] Term Source # 

Methods

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

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

Foldable21 Hakaru Hakaru [Hakaru] Lazy Source # 

Methods

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

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

Foldable21 Hakaru Hakaru [Hakaru] Whnf Source # 

Methods

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

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

Foldable21 Hakaru Hakaru [Hakaru] Head Source # 

Methods

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

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

Functor21 Hakaru Hakaru [Hakaru] Term Source # 

Methods

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

Functor21 Hakaru Hakaru [Hakaru] Lazy Source # 

Methods

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

Functor21 Hakaru Hakaru [Hakaru] Whnf Source # 

Methods

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

Functor21 Hakaru Hakaru [Hakaru] Head Source # 

Methods

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

Traversable21 Hakaru Hakaru [Hakaru] (Branch a) Source # 

Methods

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

Foldable21 Hakaru Hakaru [Hakaru] (Branch a) Source # 

Methods

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

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

Functor21 Hakaru Hakaru [Hakaru] (Branch a) Source # 

Methods

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

JmEq1 Hakaru (Sing Hakaru) Source # 

Methods

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

JmEq1 Hakaru (PrimCoercion a) Source # 

Methods

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

Eq1 Hakaru ast => JmEq1 Hakaru (Datum ast) Source # 

Methods

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

Eq1 Hakaru (Sing Hakaru) Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru (Coercion a) Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru (PrimCoercion a) Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru (Pattern vars) Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru ast => Eq1 Hakaru (Datum ast) Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru (MeasureOp typs) Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru (ArrayOp args) Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru (PrimOp args) Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Show1 Hakaru (Sing Hakaru) Source # 

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

Show1 Hakaru (Pattern vars) Source # 

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

Show1 Hakaru ast => Show1 Hakaru (Datum ast) Source # 

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

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

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

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

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

SingI Hakaru a => SingI Hakaru (HMeasure a) Source # 

Methods

sing :: Sing (HMeasure a) a Source #

SingI Hakaru a => SingI Hakaru (HArray a) Source # 

Methods

sing :: Sing (HArray a) a Source #

JmEq2 Hakaru [Hakaru] MeasureOp Source # 

Methods

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

JmEq2 Hakaru [Hakaru] ArrayOp Source # 

Methods

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

JmEq2 Hakaru [Hakaru] PrimOp Source # 

Methods

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

Eq2 Hakaru [Hakaru] Pattern Source # 

Methods

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

Eq2 Hakaru [Hakaru] MeasureOp Source # 

Methods

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

Eq2 Hakaru [Hakaru] ArrayOp Source # 

Methods

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

Eq2 Hakaru [Hakaru] PrimOp Source # 

Methods

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

Show2 Hakaru [Hakaru] Pattern Source # 

Methods

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

show2 :: a i j -> String Source #

Eq2 Hakaru [Hakaru] (PDatumFun x) Source # 

Methods

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

Eq2 Hakaru [Hakaru] (PDatumStruct xs) Source # 

Methods

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

Eq2 Hakaru [Hakaru] (PDatumCode xss) Source # 

Methods

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

Show2 Hakaru [Hakaru] (PDatumFun x) Source # 

Methods

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

show2 :: a i j -> String Source #

Show2 Hakaru [Hakaru] (PDatumStruct xs) Source # 

Methods

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

show2 :: a i j -> String Source #

Show2 Hakaru [Hakaru] (PDatumCode xss) Source # 

Methods

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

show2 :: a i j -> String Source #

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

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru (PDatumFun x vars) Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru (PDatumStruct xs vars) Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 Hakaru (PDatumCode xss vars) Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

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

Methods

eq1 :: a i -> a i -> Bool Source #

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

Methods

eq1 :: a i -> a i -> Bool Source #

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

Methods

eq1 :: a i -> a i -> Bool Source #

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

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

Show1 Hakaru (PDatumFun x vars) Source # 

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

Show1 Hakaru (PDatumStruct xs vars) Source # 

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

Show1 Hakaru (PDatumCode xss vars) Source # 

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

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

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

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

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

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

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

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

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

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

Methods

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

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

Methods

sing :: Sing (HData t sop) a Source #

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) Source # 
PrimCoerce (Sing Hakaru) Source # 
Traversable21 [([Hakaru], Hakaru)] Hakaru [Hakaru] SArgs Source # 

Methods

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

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

Methods

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

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

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

Methods

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

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

Methods

eq1 :: a i -> a i -> Bool Source #

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

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

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 Source #

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

data HakaruFun Source #

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 Source # 

Methods

hOrd :: HOrd HUnit Source #

HOrd_ HBool Source # 

Methods

hOrd :: HOrd HBool Source #

HEq_ HUnit Source # 

Methods

hEq :: HEq HUnit Source #

HEq_ HBool Source # 

Methods

hEq :: HEq HBool Source #

SingI HakaruFun I Source # 

Methods

sing :: Sing I a Source #

Interp HUnit () Source # 

Methods

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

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

Interp HBool Bool Source # 

Methods

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

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

JmEq1 HakaruFun (Sing HakaruFun) Source # 

Methods

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

Eq1 HakaruFun (Sing HakaruFun) Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Show1 HakaruFun (Sing HakaruFun) Source # 

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

SingI Hakaru a => SingI HakaruFun (K a) Source # 

Methods

sing :: Sing (K a) a Source #

JmEq1 [[HakaruFun]] (Sing [[HakaruFun]]) Source # 

Methods

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

JmEq1 [HakaruFun] (Sing [HakaruFun]) Source # 

Methods

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

Eq1 [[HakaruFun]] (Sing [[HakaruFun]]) Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Eq1 [HakaruFun] (Sing [HakaruFun]) Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Show1 [[HakaruFun]] (Sing [[HakaruFun]]) Source # 

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

Show1 [HakaruFun] (Sing [HakaruFun]) Source # 

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

SingI [[HakaruFun]] ([] [HakaruFun]) Source # 

Methods

sing :: Sing [[HakaruFun]] a Source #

SingI [HakaruFun] ([] HakaruFun) Source # 

Methods

sing :: Sing [HakaruFun] a Source #

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

Methods

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

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

Methods

sing :: Sing ((HakaruFun ': x) xs) a Source #

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) # 
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) # 
(HOrd_ a, HOrd_ b) => HOrd_ (HEither a b) Source # 

Methods

hOrd :: HOrd (HEither a b) Source #

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

Methods

hOrd :: HOrd (HPair a b) Source #

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

Methods

hEq :: HEq (HEither a b) Source #

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

Methods

hEq :: HEq (HPair a b) Source #

data Sing HakaruFun Source # 
data Sing [[HakaruFun]] Source # 
data Sing [[HakaruFun]] where
data Sing [HakaruFun] Source # 
data Sing [HakaruFun] where

data HakaruCon Source #

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 

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 Source # 

Methods

sing :: Sing s a Source #

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) Source # 

Methods

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

Eq1 Symbol (Sing Symbol) Source # 

Methods

eq1 :: a i -> a i -> Bool Source #

Show1 Symbol (Sing Symbol) Source # 

Methods

showsPrec1 :: Int -> a i -> ShowS Source #

show1 :: a i -> String Source #

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

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]] Source #

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") Source # 
type Code (TyCon "Bool") = (:) [HakaruFun] ([] HakaruFun) ((:) [HakaruFun] ([] HakaruFun) ([] [HakaruFun]))
type Code (TyCon "Unit") Source # 
type Code (TyCon "Unit") = (:) [HakaruFun] ([] HakaruFun) ([] [HakaruFun])
type Code ((:@) (TyCon "List") a) Source # 
type Code ((:@) (TyCon "List") a) = (:) [HakaruFun] ([] HakaruFun) ((:) [HakaruFun] ((:) HakaruFun (K a) ((:) HakaruFun I ([] HakaruFun))) ([] [HakaruFun]))
type Code ((:@) (TyCon "Maybe") a) Source # 
type Code ((:@) (TyCon "Maybe") a) = (:) [HakaruFun] ([] HakaruFun) ((:) [HakaruFun] ((:) HakaruFun (K a) ([] HakaruFun)) ([] [HakaruFun]))
type Code ((:@) ((:@) (TyCon "Either") a) b) Source # 
type Code ((:@) ((:@) (TyCon "Either") a) b) = (:) [HakaruFun] ((:) HakaruFun (K a) ([] HakaruFun)) ((:) [HakaruFun] ((:) HakaruFun (K b) ([] HakaruFun)) ([] [HakaruFun]))
type Code ((:@) ((:@) (TyCon "Pair") a) b) Source # 
type Code ((:@) ((:@) (TyCon "Pair") a) b) = (:) [HakaruFun] ((:) HakaruFun (K a) ((:) HakaruFun (K b) ([] HakaruFun))) ([] [HakaruFun])

type HData' t = HData t (Code t) Source #

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") '['[], '[]] Source #

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

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

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

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

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