hakaru-0.3.0: A probabilistic programming language

Language.Hakaru.Types.DataKind

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

 # Methodsid :: cat a a #(.) :: cat b c -> cat a b -> cat a c # Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq HContinuous i j) Source # Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq HDiscrete i j) Source # Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq HIntegrable i j) Source # Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq HRadical i j) Source # Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq HFractional i j) Source # Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq HRing i j) Source # Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq HSemiring i j) Source # Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq NaryOp i j) Source # Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq Literal i j) Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # Source # Methods Source # Methods Source # Methods Source # Methods Source # Methodstraverse11 :: Applicative f => (forall i. a i -> f (b i)) -> t a j -> f (t b j) Source # Source # Methodsfold11 :: Monoid m => f (Lift1 k1 m) i -> m Source #foldMap11 :: Monoid m => (forall i. a i -> m) -> f a j -> m Source # Source # Methodsfmap11 :: (forall i. a i -> b i) -> f a j -> f b j Source # Source # MethodsjmEq2 :: a i1 j1 -> a i2 j2 -> Maybe (TypeEq k1 i1 i2, TypeEq PrimCoercion j1 j2) Source # Source # Methodseq2 :: a i j -> a i j -> Bool Source # Source # Methodseq2 :: a i j -> a i j -> Bool Source # Source # Methodstraverse11 :: Applicative f => (forall i. a i -> f (b i)) -> t a j -> f (t b j) Source # Source # Methodstraverse11 :: Applicative f => (forall i. a i -> f (b i)) -> t a j -> f (t b j) Source # Source # Methodstraverse11 :: Applicative f => (forall i. a i -> f (b i)) -> t a j -> f (t b j) Source # Source # Methodsfold11 :: Monoid m => f (Lift1 k1 m) i -> m Source #foldMap11 :: Monoid m => (forall i. a i -> m) -> f a j -> m Source # Source # Methodsfold11 :: Monoid m => f (Lift1 k1 m) i -> m Source #foldMap11 :: Monoid m => (forall i. a i -> m) -> f a j -> m Source # Source # Methodsfold11 :: Monoid m => f (Lift1 k1 m) i -> m Source #foldMap11 :: Monoid m => (forall i. a i -> m) -> f a j -> m Source # Source # Methodsfmap11 :: (forall i. a i -> b i) -> f a j -> f b j Source # Source # Methodsfmap11 :: (forall i. a i -> b i) -> f a j -> f b j Source # Source # Methodsfmap11 :: (forall i. a i -> b i) -> f a j -> f b j Source # Source # Methodstraverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j) Source # Source # Methodstraverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j) Source # Source # Methodstraverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j) Source # Source # Methodstraverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j) Source # Source # Methodsfold21 :: 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 # Source # Methodsfold21 :: 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 # Source # Methodsfold21 :: 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 # Source # Methodsfold21 :: 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 # Source # Methodsfmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j Source # Source # Methodsfmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j Source # Source # Methodsfmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j Source # Source # Methodsfmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j Source # Source # Methodstraverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j) Source # Source # Methodsfold21 :: 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 # Source # Methodsfmap21 :: (forall h i. a h i -> b h i) -> f a j -> f b j Source # Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq (Sing Hakaru) i j) Source # Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq (PrimCoercion a) i j) Source # Eq1 Hakaru ast => JmEq1 Hakaru (Datum ast) Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq (Datum ast) i j) Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Eq1 Hakaru (Pattern vars) Source # Methodseq1 :: a i -> a i -> Bool Source # Eq1 Hakaru ast => Eq1 Hakaru (Datum ast) Source # Methodseq1 :: a i -> a i -> Bool Source # Eq1 Hakaru (MeasureOp typs) Source # Methodseq1 :: a i -> a i -> Bool Source # Eq1 Hakaru (ArrayOp args) Source # Methodseq1 :: a i -> a i -> Bool Source # Eq1 Hakaru (PrimOp args) Source # Methodseq1 :: a i -> a i -> Bool Source # Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # Show1 Hakaru (Pattern vars) Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # Show1 Hakaru ast => Show1 Hakaru (Datum ast) Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # Show2 Hakaru [Hakaru] abt => Show1 Hakaru (LC_ abt) Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # Show2 Hakaru [Hakaru] abt => Show1 Hakaru (Term abt) Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # Source # Methodssing :: Sing (HMeasure a) a Source # SingI Hakaru a => SingI Hakaru (HArray a) Source # Methodssing :: Sing (HArray a) a Source # Source # MethodsjmEq2 :: a i1 j1 -> a i2 j2 -> Maybe (TypeEq k1 i1 i2, TypeEq MeasureOp j1 j2) Source # Source # MethodsjmEq2 :: a i1 j1 -> a i2 j2 -> Maybe (TypeEq k1 i1 i2, TypeEq ArrayOp j1 j2) Source # Source # MethodsjmEq2 :: a i1 j1 -> a i2 j2 -> Maybe (TypeEq k1 i1 i2, TypeEq PrimOp j1 j2) Source # Source # Methodseq2 :: a i j -> a i j -> Bool Source # Source # Methodseq2 :: a i j -> a i j -> Bool Source # Source # Methodseq2 :: a i j -> a i j -> Bool Source # Source # Methodseq2 :: a i j -> a i j -> Bool Source # Source # MethodsshowsPrec2 :: Int -> a i j -> ShowS Source #show2 :: a i j -> String Source # Eq2 Hakaru [Hakaru] (PDatumFun x) Source # Methodseq2 :: a i j -> a i j -> Bool Source # Eq2 Hakaru [Hakaru] (PDatumStruct xs) Source # Methodseq2 :: a i j -> a i j -> Bool Source # Eq2 Hakaru [Hakaru] (PDatumCode xss) Source # Methodseq2 :: a i j -> a i j -> Bool Source # Source # MethodsshowsPrec2 :: Int -> a i j -> ShowS Source #show2 :: a i j -> String Source # Source # MethodsshowsPrec2 :: Int -> a i j -> ShowS Source #show2 :: a i j -> String Source # Show2 Hakaru [Hakaru] (PDatumCode xss) Source # MethodsshowsPrec2 :: Int -> a i j -> ShowS Source #show2 :: a i j -> String Source # Eq2 Hakaru [Hakaru] abt => Eq1 Hakaru (Branch a abt) Source # Methodseq1 :: a i -> a i -> Bool Source # Eq1 Hakaru (PDatumFun x vars) Source # Methodseq1 :: a i -> a i -> Bool Source # Eq1 Hakaru (PDatumStruct xs vars) Source # Methodseq1 :: a i -> a i -> Bool Source # Eq1 Hakaru (PDatumCode xss vars) Source # Methodseq1 :: a i -> a i -> Bool Source # Eq1 Hakaru ast => Eq1 Hakaru (DatumFun x ast) Source # Methodseq1 :: a i -> a i -> Bool Source # Eq1 Hakaru ast => Eq1 Hakaru (DatumStruct xs ast) Source # Methodseq1 :: a i -> a i -> Bool Source # Eq1 Hakaru ast => Eq1 Hakaru (DatumCode xss ast) Source # Methodseq1 :: a i -> a i -> Bool Source # Show2 Hakaru [Hakaru] abt => Show1 Hakaru (Branch a abt) Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # Show1 Hakaru (PDatumFun x vars) Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # Show1 Hakaru (PDatumStruct xs vars) Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # Show1 Hakaru (PDatumCode xss vars) Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # Show1 Hakaru ast => Show1 Hakaru (DatumFun x ast) Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # Show1 Hakaru ast => Show1 Hakaru (DatumStruct xs ast) Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # Show1 Hakaru ast => Show1 Hakaru (DatumCode xss ast) Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # (Show1 Hakaru ast, Show2 Hakaru [Hakaru] abt) => Show1 Hakaru (MatchResult ast abt) Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # (SingI Hakaru a, SingI Hakaru b) => SingI Hakaru ((:->) a b) Source # Methodssing :: Sing (a :-> b) a Source # ((~) [[HakaruFun]] sop (Code t), SingI HakaruCon t, SingI [[HakaruFun]] sop) => SingI Hakaru (HData t sop) Source # Methodssing :: 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))) # Methodscompare :: 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]) # Source # MethodscoerceTo :: Coercion a b -> Sing Hakaru a -> Sing Hakaru b Source #coerceFrom :: Coercion a b -> Sing Hakaru b -> Sing Hakaru a Source # Source # MethodsprimCoerceTo :: PrimCoercion a b -> Sing Hakaru a -> Sing Hakaru b Source # Source # Methodstraverse21 :: Applicative f => (forall h i. a h i -> f (b h i)) -> t a j -> f (t b j) Source # Source # Methodsfold21 :: 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 # Source # Methodsfmap21 :: (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 # Methodseq1 :: a i -> a i -> Bool Source # Show2 Hakaru [Hakaru] abt => Show1 [([Hakaru], Hakaru)] (SArgs abt) Source # MethodsshowsPrec1 :: 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 # # MethodsshowsPrec :: 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 Sing Hakaru whereSNat :: Sing Hakaru HNatSInt :: Sing Hakaru HIntSProb :: Sing Hakaru HProbSReal :: Sing Hakaru HRealSMeasure :: Sing Hakaru (HMeasure a)SArray :: Sing Hakaru (HArray a)SFun :: Sing Hakaru ((:->) a b)SData :: Sing Hakaru (HData' t)

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

 Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methodsreify :: ABT Hakaru Term abt => Head abt HUnit -> () Source #reflect :: ABT Hakaru Term abt => () -> Head abt HUnit Source # Source # Methodsreify :: ABT Hakaru Term abt => Head abt HBool -> Bool Source #reflect :: ABT Hakaru Term abt => Bool -> Head abt HBool Source # Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq (Sing HakaruFun) i j) Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # SingI Hakaru a => SingI HakaruFun (K a) Source # Methodssing :: Sing (K a) a Source # JmEq1 [[HakaruFun]] (Sing [[HakaruFun]]) Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq (Sing [[HakaruFun]]) i j) Source # JmEq1 [HakaruFun] (Sing [HakaruFun]) Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq (Sing [HakaruFun]) i j) Source # Eq1 [[HakaruFun]] (Sing [[HakaruFun]]) Source # Methodseq1 :: a i -> a i -> Bool Source # Eq1 [HakaruFun] (Sing [HakaruFun]) Source # Methodseq1 :: a i -> a i -> Bool Source # Show1 [[HakaruFun]] (Sing [[HakaruFun]]) Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # Show1 [HakaruFun] (Sing [HakaruFun]) Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # SingI [[HakaruFun]] ([] [HakaruFun]) Source # Methodssing :: Sing [[HakaruFun]] a Source # SingI [HakaruFun] ([] HakaruFun) Source # Methodssing :: Sing [HakaruFun] a Source # (SingI [HakaruFun] xs, SingI [[HakaruFun]] xss) => SingI [[HakaruFun]] ((:) [HakaruFun] xs xss) Source # Methodssing :: Sing (([HakaruFun] ': xs) xss) a Source # (SingI HakaruFun x, SingI [HakaruFun] xs) => SingI [HakaruFun] ((:) HakaruFun x xs) Source # Methodssing :: 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 # # Methods(==) :: Sing HakaruFun a -> Sing HakaruFun a -> Bool #(/=) :: Sing HakaruFun a -> Sing HakaruFun a -> Bool # Show (Sing [[HakaruFun]] a) # MethodsshowsPrec :: Int -> Sing [[HakaruFun]] a -> ShowS #show :: Sing [[HakaruFun]] a -> String #showList :: [Sing [[HakaruFun]] a] -> ShowS # Show (Sing [HakaruFun] a) # MethodsshowsPrec :: Int -> Sing [HakaruFun] a -> ShowS #show :: Sing [HakaruFun] a -> String #showList :: [Sing [HakaruFun] a] -> ShowS # # MethodsshowsPrec :: Int -> Sing HakaruFun a -> ShowS #show :: Sing HakaruFun a -> String #showList :: [Sing HakaruFun a] -> ShowS # (HOrd_ a, HOrd_ b) => HOrd_ (HEither a b) Source # MethodshOrd :: HOrd (HEither a b) Source # (HOrd_ a, HOrd_ b) => HOrd_ (HPair a b) Source # MethodshOrd :: HOrd (HPair a b) Source # (HEq_ a, HEq_ b) => HEq_ (HEither a b) Source # MethodshEq :: HEq (HEither a b) Source # (HEq_ a, HEq_ b) => HEq_ (HPair a b) Source # MethodshEq :: HEq (HPair a b) Source # data Sing HakaruFun Source # data Sing HakaruFun whereSIdent :: Sing HakaruFun ISKonst :: Sing HakaruFun (K a) data Sing [[HakaruFun]] Source # data Sing [[HakaruFun]] whereSVoid :: Sing [[HakaruFun]] ([] [HakaruFun])SPlus :: Sing [[HakaruFun]] ((:) [HakaruFun] xs xss) data Sing [HakaruFun] Source # data Sing [HakaruFun] whereSDone :: Sing [HakaruFun] ([] HakaruFun)SEt :: Sing [HakaruFun] ((:) HakaruFun x xs)

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

Instances

 Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq (Sing HakaruCon) i j) Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Source # MethodsshowsPrec1 :: Int -> a i -> ShowS Source #show1 :: a i -> String Source # Source # Methodssing :: Sing (TyCon s) a Source # (SingI HakaruCon a, SingI Hakaru b) => SingI HakaruCon ((:@) a b) Source # Methodssing :: Sing (a :@ b) a Source # # Methods(==) :: Sing HakaruCon a -> Sing HakaruCon a -> Bool #(/=) :: Sing HakaruCon a -> Sing HakaruCon a -> Bool # # MethodsshowsPrec :: Int -> Sing HakaruCon a -> ShowS #show :: Sing HakaruCon a -> String #showList :: [Sing HakaruCon a] -> ShowS # data Sing HakaruCon Source # data Sing HakaruCon whereSTyCon :: 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 Methodssing :: Sing a a Source # Methodssing :: Sing s a Source # SingKind Symbol (KProxy Symbol) Associated Typestype DemoteRep (KProxy Symbol) (kparam :: KProxy (KProxy Symbol)) :: * MethodsfromSing :: Sing (KProxy Symbol) a -> DemoteRep (KProxy Symbol) kparam Source # MethodsjmEq1 :: a i -> a j -> Maybe (TypeEq (Sing Symbol) i j) Source # Source # Methodseq1 :: a i -> a i -> Bool Source # Source # MethodsshowsPrec1 :: 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 # # MethodsshowsPrec :: Int -> Sing Symbol s -> ShowS #show :: Sing Symbol s -> String #showList :: [Sing Symbol s] -> ShowS # data Sing Symbol data Sing Symbol whereSSym :: Sing Symbol s 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). data Sing Symbol whereSingSymbol :: 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]] 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 #