Copyright	Copyright (c) 2016 the Hakaru team
License	BSD3
Maintainer	wren@community.haskell.org
Stability	experimental
Portability	GHC-only
Safe Haskell	None
Language	Haskell2010

Language.Hakaru.Syntax.Datum

Contents

Data constructors
- Some smart constructors for the "built-in" datatypes
  - Variants which allow explicit type passing.
Pattern constructors
- Some smart constructors for the "built-in" datatypes
- Generalized branches

Description

Haskell types and helpers for Hakaru's user-defined data types. At present we only support regular-recursive polynomial data types. Reduction of case analysis on data types is in Language.Hakaru.Syntax.Datum.

Developers note: many of the JmEq1 instances in this file don't actually work because of problems with matching existentially quantified types in the basis cases. For now I've left the partially-defined code in place, but turned it off with the PARTIAL_DATUM_JMEQ CPP macro. In the future we should either (a) remove this unused code, or (b) if the instances are truly necessary then we should add the Sing arguments everywhere to make things work :(

Synopsis

data Datum :: (Hakaru -> *) -> Hakaru -> * where
- Datum :: !Text -> !(Sing (HData' t)) -> !(DatumCode (Code t) ast (HData' t)) -> Datum ast (HData' t)
datumHint :: Datum ast (HData' t) -> Text
datumType :: Datum ast (HData' t) -> Sing (HData' t)
data DatumCode :: [[HakaruFun]] -> (Hakaru -> *) -> Hakaru -> * where
- Inr :: !(DatumCode xss abt a) -> DatumCode (xs ': xss) abt a
- Inl :: !(DatumStruct xs abt a) -> DatumCode (xs ': xss) abt a
data DatumStruct :: [HakaruFun] -> (Hakaru -> *) -> Hakaru -> * where
- Et :: !(DatumFun x abt a) -> !(DatumStruct xs abt a) -> DatumStruct (x ': xs) abt a
- Done :: DatumStruct '[] abt a
data DatumFun :: HakaruFun -> (Hakaru -> *) -> Hakaru -> * where
- Konst :: !(ast b) -> DatumFun ('K b) ast a
- Ident :: !(ast a) -> DatumFun 'I ast a
dTrue :: Datum ast HBool
dFalse :: Datum ast HBool
dBool :: Bool -> Datum ast HBool
dUnit :: Datum ast HUnit
dPair :: (SingI a, SingI b) => ast a -> ast b -> Datum ast (HPair a b)
dLeft :: (SingI a, SingI b) => ast a -> Datum ast (HEither a b)
dRight :: (SingI a, SingI b) => ast b -> Datum ast (HEither a b)
dNil :: SingI a => Datum ast (HList a)
dCons :: SingI a => ast a -> ast (HList a) -> Datum ast (HList a)
dNothing :: SingI a => Datum ast (HMaybe a)
dJust :: SingI a => ast a -> Datum ast (HMaybe a)
dPair_ :: Sing a -> Sing b -> ast a -> ast b -> Datum ast (HPair a b)
dLeft_ :: Sing a -> Sing b -> ast a -> Datum ast (HEither a b)
dRight_ :: Sing a -> Sing b -> ast b -> Datum ast (HEither a b)
dNil_ :: Sing a -> Datum ast (HList a)
dCons_ :: Sing a -> ast a -> ast (HList a) -> Datum ast (HList a)
dNothing_ :: Sing a -> Datum ast (HMaybe a)
dJust_ :: Sing a -> ast a -> Datum ast (HMaybe a)
data Branch (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *) (b :: Hakaru) = forall xs. Branch !(Pattern xs a) !(abt xs b)
data Pattern :: [Hakaru] -> Hakaru -> * where
- PWild :: Pattern '[] a
- PVar :: Pattern '[a] a
- PDatum :: !Text -> !(PDatumCode (Code t) vars (HData' t)) -> Pattern vars (HData' t)
data PDatumCode :: [[HakaruFun]] -> [Hakaru] -> Hakaru -> * where
- PInr :: !(PDatumCode xss vars a) -> PDatumCode (xs ': xss) vars a
- PInl :: !(PDatumStruct xs vars a) -> PDatumCode (xs ': xss) vars a
data PDatumStruct :: [HakaruFun] -> [Hakaru] -> Hakaru -> * where
- PEt :: !(PDatumFun x vars1 a) -> !(PDatumStruct xs vars2 a) -> PDatumStruct (x ': xs) (vars1 ++ vars2) a
- PDone :: PDatumStruct '[] '[] a
data PDatumFun :: HakaruFun -> [Hakaru] -> Hakaru -> * where
- PKonst :: !(Pattern vars b) -> PDatumFun ('K b) vars a
- PIdent :: !(Pattern vars a) -> PDatumFun 'I vars a
pTrue :: Pattern '[] HBool
pFalse :: Pattern '[] HBool
pUnit :: Pattern '[] HUnit
pPair :: Pattern vars1 a -> Pattern vars2 b -> Pattern (vars1 ++ vars2) (HPair a b)
pLeft :: Pattern vars a -> Pattern vars (HEither a b)
pRight :: Pattern vars b -> Pattern vars (HEither a b)
pNil :: Pattern '[] (HList a)
pCons :: Pattern vars1 a -> Pattern vars2 (HList a) -> Pattern (vars1 ++ vars2) (HList a)
pNothing :: Pattern '[] (HMaybe a)
pJust :: Pattern vars a -> Pattern vars (HMaybe a)
data GBranch (a :: Hakaru) (r :: *) = forall xs. GBranch !(Pattern xs a) !(List1 Variable xs) r

Data constructors

data Datum :: (Hakaru -> *) -> Hakaru -> * where Source #

A fully saturated data constructor, which recurses as ast. We define this type as separate from DatumCode for two reasons. First is to capture the fact that the datum is "complete" (i.e., is a well-formed constructor). The second is to have a type which is indexed by its Hakaru type, whereas DatumCode involves non-Hakaru types.

The first component is a hint for what the data constructor should be called when pretty-printing, giving error messages, etc. Like the hints for variable names, its value is not actually used to decide which constructor is meant or which pattern matches.

Constructors

Datum :: !Text -> !(Sing (HData' t)) -> !(DatumCode (Code t) ast (HData' t)) -> Datum ast (HData' t)

Instances

Instances details

Traversable11 Datum Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods traverse11 :: forall f a b (j :: k2). Applicative f => (forall (i :: k1). a i -> f (b i)) -> Datum a j -> f (Datum b j) Source #
Foldable11 Datum Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods fold11 :: forall m (i :: k2). Monoid m => Datum (Lift1 m) i -> m Source # foldMap11 :: forall m a (j :: k2). Monoid m => (forall (i :: k1). a i -> m) -> Datum a j -> m Source #
Functor11 Datum Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods fmap11 :: forall a b (j :: k2). (forall (i :: k1). a i -> b i) -> Datum a j -> Datum b j Source #
Eq1 ast => JmEq1 (Datum ast :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods jmEq1 :: forall (i :: k) (j :: k). Datum ast i -> Datum ast j -> Maybe (TypeEq i j) Source #
Eq1 ast => Eq1 (Datum ast :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods eq1 :: forall (i :: k). Datum ast i -> Datum ast i -> Bool Source #
Show1 ast => Show1 (Datum ast :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec1 :: forall (i :: k). Int -> Datum ast i -> ShowS Source # show1 :: forall (i :: k). Datum ast i -> String Source #
Pretty f => Pretty (Datum f) Source #
Instance details Defined in Language.Hakaru.Pretty.Haskell Methods prettyPrec_ :: forall (a :: Hakaru). Int -> Datum f a -> Docs Source #
Eq1 ast => Eq (Datum ast a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods (==) :: Datum ast a -> Datum ast a -> Bool # (/=) :: Datum ast a -> Datum ast a -> Bool #
Show1 ast => Show (Datum ast a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec :: Int -> Datum ast a -> ShowS # show :: Datum ast a -> String # showList :: [Datum ast a] -> ShowS #

datumHint :: Datum ast (HData' t) -> Text Source #

datumType :: Datum ast (HData' t) -> Sing (HData' t) Source #

data DatumCode :: [[HakaruFun]] -> (Hakaru -> *) -> Hakaru -> * where Source #

The intermediate components of a data constructor. The intuition behind the two indices is that the [[HakaruFun]] is a functor applied to the Hakaru type. Initially the [[HakaruFun]] functor will be the Code associated with the Hakaru type; hence it's the one-step unrolling of the fixed point for our recursive datatypes. But as we go along, we'll be doing induction on the [[HakaruFun]] functor.

Constructors

Inr :: !(DatumCode xss abt a) -> DatumCode (xs ': xss) abt a
Inl :: !(DatumStruct xs abt a) -> DatumCode (xs ': xss) abt a

Instances

Instances details

Traversable11 (DatumCode xss :: (Hakaru -> Type) -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods traverse11 :: forall f a b (j :: k2). Applicative f => (forall (i :: k1). a i -> f (b i)) -> DatumCode xss a j -> f (DatumCode xss b j) Source #
Foldable11 (DatumCode xss :: (Hakaru -> Type) -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods fold11 :: forall m (i :: k2). Monoid m => DatumCode xss (Lift1 m) i -> m Source # foldMap11 :: forall m a (j :: k2). Monoid m => (forall (i :: k1). a i -> m) -> DatumCode xss a j -> m Source #
Functor11 (DatumCode xss :: (Hakaru -> Type) -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods fmap11 :: forall a b (j :: k2). (forall (i :: k1). a i -> b i) -> DatumCode xss a j -> DatumCode xss b j Source #
Eq1 ast => Eq1 (DatumCode xss ast :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods eq1 :: forall (i :: k). DatumCode xss ast i -> DatumCode xss ast i -> Bool Source #
Show1 ast => Show1 (DatumCode xss ast :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec1 :: forall (i :: k). Int -> DatumCode xss ast i -> ShowS Source # show1 :: forall (i :: k). DatumCode xss ast i -> String Source #
Eq1 ast => Eq (DatumCode xss ast a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods (==) :: DatumCode xss ast a -> DatumCode xss ast a -> Bool # (/=) :: DatumCode xss ast a -> DatumCode xss ast a -> Bool #
Show1 ast => Show (DatumCode xss ast a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec :: Int -> DatumCode xss ast a -> ShowS # show :: DatumCode xss ast a -> String # showList :: [DatumCode xss ast a] -> ShowS #

data DatumStruct :: [HakaruFun] -> (Hakaru -> *) -> Hakaru -> * where Source #

Constructors

Et :: !(DatumFun x abt a) -> !(DatumStruct xs abt a) -> DatumStruct (x ': xs) abt a infixr 7
Done :: DatumStruct '[] abt a

Instances

Instances details

Traversable11 (DatumStruct xs :: (Hakaru -> Type) -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods traverse11 :: forall f a b (j :: k2). Applicative f => (forall (i :: k1). a i -> f (b i)) -> DatumStruct xs a j -> f (DatumStruct xs b j) Source #
Foldable11 (DatumStruct xs :: (Hakaru -> Type) -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods fold11 :: forall m (i :: k2). Monoid m => DatumStruct xs (Lift1 m) i -> m Source # foldMap11 :: forall m a (j :: k2). Monoid m => (forall (i :: k1). a i -> m) -> DatumStruct xs a j -> m Source #
Functor11 (DatumStruct xs :: (Hakaru -> Type) -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods fmap11 :: forall a b (j :: k2). (forall (i :: k1). a i -> b i) -> DatumStruct xs a j -> DatumStruct xs b j Source #
Eq1 ast => Eq1 (DatumStruct xs ast :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods eq1 :: forall (i :: k). DatumStruct xs ast i -> DatumStruct xs ast i -> Bool Source #
Show1 ast => Show1 (DatumStruct xs ast :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec1 :: forall (i :: k). Int -> DatumStruct xs ast i -> ShowS Source # show1 :: forall (i :: k). DatumStruct xs ast i -> String Source #
Eq1 ast => Eq (DatumStruct xs ast a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods (==) :: DatumStruct xs ast a -> DatumStruct xs ast a -> Bool # (/=) :: DatumStruct xs ast a -> DatumStruct xs ast a -> Bool #
Show1 ast => Show (DatumStruct xs ast a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec :: Int -> DatumStruct xs ast a -> ShowS # show :: DatumStruct xs ast a -> String # showList :: [DatumStruct xs ast a] -> ShowS #

data DatumFun :: HakaruFun -> (Hakaru -> *) -> Hakaru -> * where Source #

Constructors

Konst :: !(ast b) -> DatumFun ('K b) ast a
Ident :: !(ast a) -> DatumFun 'I ast a

Instances

Instances details

Traversable11 (DatumFun x :: (Hakaru -> Type) -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods traverse11 :: forall f a b (j :: k2). Applicative f => (forall (i :: k1). a i -> f (b i)) -> DatumFun x a j -> f (DatumFun x b j) Source #
Foldable11 (DatumFun x :: (Hakaru -> Type) -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods fold11 :: forall m (i :: k2). Monoid m => DatumFun x (Lift1 m) i -> m Source # foldMap11 :: forall m a (j :: k2). Monoid m => (forall (i :: k1). a i -> m) -> DatumFun x a j -> m Source #
Functor11 (DatumFun x :: (Hakaru -> Type) -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods fmap11 :: forall a b (j :: k2). (forall (i :: k1). a i -> b i) -> DatumFun x a j -> DatumFun x b j Source #
Eq1 ast => Eq1 (DatumFun x ast :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods eq1 :: forall (i :: k). DatumFun x ast i -> DatumFun x ast i -> Bool Source #
Show1 ast => Show1 (DatumFun x ast :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec1 :: forall (i :: k). Int -> DatumFun x ast i -> ShowS Source # show1 :: forall (i :: k). DatumFun x ast i -> String Source #
Eq1 ast => Eq (DatumFun x ast a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods (==) :: DatumFun x ast a -> DatumFun x ast a -> Bool # (/=) :: DatumFun x ast a -> DatumFun x ast a -> Bool #
Show1 ast => Show (DatumFun x ast a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec :: Int -> DatumFun x ast a -> ShowS # show :: DatumFun x ast a -> String # showList :: [DatumFun x ast a] -> ShowS #

Some smart constructors for the "built-in" datatypes

dTrue :: Datum ast HBool Source #

dFalse :: Datum ast HBool Source #

dBool :: Bool -> Datum ast HBool Source #

dUnit :: Datum ast HUnit Source #

dPair :: (SingI a, SingI b) => ast a -> ast b -> Datum ast (HPair a b) Source #

dLeft :: (SingI a, SingI b) => ast a -> Datum ast (HEither a b) Source #

dRight :: (SingI a, SingI b) => ast b -> Datum ast (HEither a b) Source #

dNil :: SingI a => Datum ast (HList a) Source #

dCons :: SingI a => ast a -> ast (HList a) -> Datum ast (HList a) Source #

dNothing :: SingI a => Datum ast (HMaybe a) Source #

dJust :: SingI a => ast a -> Datum ast (HMaybe a) Source #

Variants which allow explicit type passing.

dPair_ :: Sing a -> Sing b -> ast a -> ast b -> Datum ast (HPair a b) Source #

dLeft_ :: Sing a -> Sing b -> ast a -> Datum ast (HEither a b) Source #

dRight_ :: Sing a -> Sing b -> ast b -> Datum ast (HEither a b) Source #

dNil_ :: Sing a -> Datum ast (HList a) Source #

dCons_ :: Sing a -> ast a -> ast (HList a) -> Datum ast (HList a) Source #

dNothing_ :: Sing a -> Datum ast (HMaybe a) Source #

dJust_ :: Sing a -> ast a -> Datum ast (HMaybe a) Source #

Pattern constructors

data Branch (a :: Hakaru) (abt :: [Hakaru] -> Hakaru -> *) (b :: Hakaru) Source #

Constructors

forall xs. Branch !(Pattern xs a) !(abt xs b)

Instances

Instances details

Eq2 abt => Eq1 (Branch a abt :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods eq1 :: forall (i :: k). Branch a abt i -> Branch a abt i -> Bool Source #
Show2 abt => Show1 (Branch a abt :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec1 :: forall (i :: k). Int -> Branch a abt i -> ShowS Source # show1 :: forall (i :: k). Branch a abt i -> String Source #
Traversable21 (Branch a :: ([Hakaru] -> Hakaru -> Type) -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods traverse21 :: forall f a0 b (j :: k3). Applicative f => (forall (h :: k1) (i :: k2). a0 h i -> f (b h i)) -> Branch a a0 j -> f (Branch a b j) Source #
Foldable21 (Branch a :: ([Hakaru] -> Hakaru -> Type) -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods fold21 :: forall m (j :: k3). Monoid m => Branch a (Lift2 m) j -> m Source # foldMap21 :: forall m a0 (j :: k3). Monoid m => (forall (h :: k1) (i :: k2). a0 h i -> m) -> Branch a a0 j -> m Source #
Functor21 (Branch a :: ([Hakaru] -> Hakaru -> Type) -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods fmap21 :: forall a0 b (j :: k3). (forall (h :: k1) (i :: k2). a0 h i -> b h i) -> Branch a a0 j -> Branch a b j Source #
ABT Term abt => Coerce (Branch a abt) Source #
Instance details Defined in Language.Hakaru.Syntax.TypeCheck.TypeCheckMonad Methods coerceTo :: forall (a0 :: Hakaru) (b :: Hakaru). Coercion a0 b -> Branch a abt a0 -> Branch a abt b Source # coerceFrom :: forall (a0 :: Hakaru) (b :: Hakaru). Coercion a0 b -> Branch a abt b -> Branch a abt a0 Source #
ABT Term abt => Pretty (Branch a abt) Source #
Instance details Defined in Language.Hakaru.Pretty.Haskell Methods prettyPrec_ :: forall (a0 :: Hakaru). Int -> Branch a abt a0 -> Docs Source #
Eq2 abt => Eq (Branch a abt b) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods (==) :: Branch a abt b -> Branch a abt b -> Bool # (/=) :: Branch a abt b -> Branch a abt b -> Bool #
Show2 abt => Show (Branch a abt b) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec :: Int -> Branch a abt b -> ShowS # show :: Branch a abt b -> String # showList :: [Branch a abt b] -> ShowS #

data Pattern :: [Hakaru] -> Hakaru -> * where Source #

We index patterns by the type they scrutinize. This requires the parser to be smart enough to build these patterns up, but then it guarantees that we can't have Case_ of patterns which can't possibly match according to our type system. In addition, we also index patterns by the type of what variables they bind, so that we can ensure that Branch will never "go wrong". Alas, this latter indexing means we can't use DatumCode, DatumStruct, and DatumFun but rather must define our own P variants for pattern matching.

Constructors

PWild :: Pattern '[] a
PVar :: Pattern '[a] a
PDatum :: !Text -> !(PDatumCode (Code t) vars (HData' t)) -> Pattern vars (HData' t)

Instances

Instances details

Eq1 (Pattern vars :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods eq1 :: forall (i :: k). Pattern vars i -> Pattern vars i -> Bool Source #
Show1 (Pattern vars :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec1 :: forall (i :: k). Int -> Pattern vars i -> ShowS Source # show1 :: forall (i :: k). Pattern vars i -> String Source #
Pretty (Pattern xs) Source #
Instance details Defined in Language.Hakaru.Pretty.Haskell Methods prettyPrec_ :: forall (a :: Hakaru). Int -> Pattern xs a -> Docs Source #
Eq2 Pattern Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods eq2 :: forall (i :: k1) (j :: k2). Pattern i j -> Pattern i j -> Bool Source #
Show2 Pattern Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec2 :: forall (i :: k1) (j :: k2). Int -> Pattern i j -> ShowS Source # show2 :: forall (i :: k1) (j :: k2). Pattern i j -> String Source #
Eq (Pattern vars a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods (==) :: Pattern vars a -> Pattern vars a -> Bool # (/=) :: Pattern vars a -> Pattern vars a -> Bool #
Show (Pattern vars a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec :: Int -> Pattern vars a -> ShowS # show :: Pattern vars a -> String # showList :: [Pattern vars a] -> ShowS #

data PDatumCode :: [[HakaruFun]] -> [Hakaru] -> Hakaru -> * where Source #

Constructors

PInr :: !(PDatumCode xss vars a) -> PDatumCode (xs ': xss) vars a
PInl :: !(PDatumStruct xs vars a) -> PDatumCode (xs ': xss) vars a

Instances

Instances details

Eq1 (PDatumCode xss vars :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods eq1 :: forall (i :: k). PDatumCode xss vars i -> PDatumCode xss vars i -> Bool Source #
Show1 (PDatumCode xss vars :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec1 :: forall (i :: k). Int -> PDatumCode xss vars i -> ShowS Source # show1 :: forall (i :: k). PDatumCode xss vars i -> String Source #
Eq2 (PDatumCode xss :: [Hakaru] -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods eq2 :: forall (i :: k1) (j :: k2). PDatumCode xss i j -> PDatumCode xss i j -> Bool Source #
Show2 (PDatumCode xss :: [Hakaru] -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec2 :: forall (i :: k1) (j :: k2). Int -> PDatumCode xss i j -> ShowS Source # show2 :: forall (i :: k1) (j :: k2). PDatumCode xss i j -> String Source #
Eq (PDatumCode xss vars a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods (==) :: PDatumCode xss vars a -> PDatumCode xss vars a -> Bool # (/=) :: PDatumCode xss vars a -> PDatumCode xss vars a -> Bool #
Show (PDatumCode xss vars a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec :: Int -> PDatumCode xss vars a -> ShowS # show :: PDatumCode xss vars a -> String # showList :: [PDatumCode xss vars a] -> ShowS #

data PDatumStruct :: [HakaruFun] -> [Hakaru] -> Hakaru -> * where Source #

Constructors

PEt :: !(PDatumFun x vars1 a) -> !(PDatumStruct xs vars2 a) -> PDatumStruct (x ': xs) (vars1 ++ vars2) a infixr 7
PDone :: PDatumStruct '[] '[] a

Instances

Instances details

Eq1 (PDatumStruct xs vars :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods eq1 :: forall (i :: k). PDatumStruct xs vars i -> PDatumStruct xs vars i -> Bool Source #
Show1 (PDatumStruct xs vars :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec1 :: forall (i :: k). Int -> PDatumStruct xs vars i -> ShowS Source # show1 :: forall (i :: k). PDatumStruct xs vars i -> String Source #
Eq2 (PDatumStruct xs :: [Hakaru] -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods eq2 :: forall (i :: k1) (j :: k2). PDatumStruct xs i j -> PDatumStruct xs i j -> Bool Source #
Show2 (PDatumStruct xs :: [Hakaru] -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec2 :: forall (i :: k1) (j :: k2). Int -> PDatumStruct xs i j -> ShowS Source # show2 :: forall (i :: k1) (j :: k2). PDatumStruct xs i j -> String Source #
Eq (PDatumStruct xs vars a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods (==) :: PDatumStruct xs vars a -> PDatumStruct xs vars a -> Bool # (/=) :: PDatumStruct xs vars a -> PDatumStruct xs vars a -> Bool #
Show (PDatumStruct xs vars a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec :: Int -> PDatumStruct xs vars a -> ShowS # show :: PDatumStruct xs vars a -> String # showList :: [PDatumStruct xs vars a] -> ShowS #

data PDatumFun :: HakaruFun -> [Hakaru] -> Hakaru -> * where Source #

Constructors

PKonst :: !(Pattern vars b) -> PDatumFun ('K b) vars a
PIdent :: !(Pattern vars a) -> PDatumFun 'I vars a

Instances

Instances details

Eq1 (PDatumFun x vars :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods eq1 :: forall (i :: k). PDatumFun x vars i -> PDatumFun x vars i -> Bool Source #
Show1 (PDatumFun x vars :: Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec1 :: forall (i :: k). Int -> PDatumFun x vars i -> ShowS Source # show1 :: forall (i :: k). PDatumFun x vars i -> String Source #
Eq2 (PDatumFun x :: [Hakaru] -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods eq2 :: forall (i :: k1) (j :: k2). PDatumFun x i j -> PDatumFun x i j -> Bool Source #
Show2 (PDatumFun x :: [Hakaru] -> Hakaru -> Type) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec2 :: forall (i :: k1) (j :: k2). Int -> PDatumFun x i j -> ShowS Source # show2 :: forall (i :: k1) (j :: k2). PDatumFun x i j -> String Source #
Eq (PDatumFun x vars a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods (==) :: PDatumFun x vars a -> PDatumFun x vars a -> Bool # (/=) :: PDatumFun x vars a -> PDatumFun x vars a -> Bool #
Show (PDatumFun x vars a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods showsPrec :: Int -> PDatumFun x vars a -> ShowS # show :: PDatumFun x vars a -> String # showList :: [PDatumFun x vars a] -> ShowS #

Some smart constructors for the "built-in" datatypes

pTrue :: Pattern '[] HBool Source #

pFalse :: Pattern '[] HBool Source #

pUnit :: Pattern '[] HUnit Source #

pPair :: Pattern vars1 a -> Pattern vars2 b -> Pattern (vars1 ++ vars2) (HPair a b) Source #

pLeft :: Pattern vars a -> Pattern vars (HEither a b) Source #

pRight :: Pattern vars b -> Pattern vars (HEither a b) Source #

pNil :: Pattern '[] (HList a) Source #

pCons :: Pattern vars1 a -> Pattern vars2 (HList a) -> Pattern (vars1 ++ vars2) (HList a) Source #

pNothing :: Pattern '[] (HMaybe a) Source #

pJust :: Pattern vars a -> Pattern vars (HMaybe a) Source #

Generalized branches

data GBranch (a :: Hakaru) (r :: *) Source #

A generalization of the Branch type to allow a "body" of any Haskell type.

Constructors

forall xs. GBranch !(Pattern xs a) !(List1 Variable xs) r

Instances

Instances details

Functor (GBranch a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods fmap :: (a0 -> b) -> GBranch a a0 -> GBranch a b # (<$) :: a0 -> GBranch a b -> GBranch a a0 #
Foldable (GBranch a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods fold :: Monoid m => GBranch a m -> m # foldMap :: Monoid m => (a0 -> m) -> GBranch a a0 -> m # foldMap' :: Monoid m => (a0 -> m) -> GBranch a a0 -> m # foldr :: (a0 -> b -> b) -> b -> GBranch a a0 -> b # foldr' :: (a0 -> b -> b) -> b -> GBranch a a0 -> b # foldl :: (b -> a0 -> b) -> b -> GBranch a a0 -> b # foldl' :: (b -> a0 -> b) -> b -> GBranch a a0 -> b # foldr1 :: (a0 -> a0 -> a0) -> GBranch a a0 -> a0 # foldl1 :: (a0 -> a0 -> a0) -> GBranch a a0 -> a0 # toList :: GBranch a a0 -> [a0] # null :: GBranch a a0 -> Bool # length :: GBranch a a0 -> Int # elem :: Eq a0 => a0 -> GBranch a a0 -> Bool # maximum :: Ord a0 => GBranch a a0 -> a0 # minimum :: Ord a0 => GBranch a a0 -> a0 # sum :: Num a0 => GBranch a a0 -> a0 # product :: Num a0 => GBranch a a0 -> a0 #
Traversable (GBranch a) Source #
Instance details Defined in Language.Hakaru.Syntax.Datum Methods traverse :: Applicative f => (a0 -> f b) -> GBranch a a0 -> f (GBranch a b) # sequenceA :: Applicative f => GBranch a (f a0) -> f (GBranch a a0) # mapM :: Monad m => (a0 -> m b) -> GBranch a a0 -> m (GBranch a b) # sequence :: Monad m => GBranch a (m a0) -> m (GBranch a a0) #