| Copyright | Copyright (c) 2016 the Hakaru team |
|---|---|
| License | BSD3 |
| Maintainer | wren@community.haskell.org |
| Stability | experimental |
| Portability | GHC-only |
| Safe Haskell | Safe |
| Language | Haskell2010 |
Language.Hakaru.Types.DataKind
Description
A data-kind for the universe of Hakaru types.
- data Hakaru
- data HakaruFun
- data HakaruCon
- data Symbol :: *
- type family Code (a :: HakaruCon) :: [[HakaruFun]]
- type HData' t = HData t (Code t)
- 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]]
The core definition of Hakaru types
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 |
| 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 |
Instances
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.
Instances
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".
Instances
| JmEq1 HakaruCon (Sing HakaruCon) Source # | |
| Eq1 HakaruCon (Sing HakaruCon) Source # | |
| Show1 HakaruCon (Sing HakaruCon) Source # | |
| KnownSymbol s => SingI HakaruCon (TyCon s) Source # | |
| (SingI HakaruCon a, SingI Hakaru b) => SingI HakaruCon ((:@) a b) Source # | |
| Eq (Sing HakaruCon a) # | |
| Show (Sing HakaruCon a) # | |
| data Sing HakaruCon Source # | |
(Kind) This is the kind of type-level symbols. Declared here because class IP needs it
Instances
| KnownSymbol a => SingI Symbol a | |
| KnownSymbol s => SingI Symbol s Source # | |
| SingKind Symbol (KProxy Symbol) | |
| JmEq1 Symbol (Sing Symbol) Source # | |
| Eq1 Symbol (Sing Symbol) Source # | |
| Show1 Symbol (Sing Symbol) Source # | |
| Eq (Sing Symbol s) # | |
| Show (Sing Symbol s) # | |
| data Sing Symbol | |
| data Sing Symbol Source # | N.B., in order to bring the |
| type (==) Symbol a b | |
| type DemoteRep Symbol (KProxy Symbol) | |
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.
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.