Language.Hakaru.Syntax.Datum

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 :(

Data constructors

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

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

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

Eq1 Hakaru ast => JmEq1 Hakaru (Datum ast)

Methods

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

Eq1 Hakaru ast => Eq1 Hakaru (Datum ast)

Methods

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

Show1 Hakaru ast => Show1 Hakaru (Datum ast)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Pretty f => Pretty (Datum f)

Methods

prettyPrec_ :: Int -> Datum f a -> Docs

Eq1 Hakaru ast => Eq (Datum ast a)

Methods

(==) :: Datum ast a -> Datum ast a -> Bool

(/=) :: Datum ast a -> Datum ast a -> Bool

Show1 Hakaru ast => Show (Datum ast a)

Methods

showsPrec :: Int -> Datum ast a -> ShowS

show :: Datum ast a -> String

showList :: [Datum ast a] -> ShowS

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

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

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

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

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 (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 (DatumCode xss)

Methods

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

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

Methods

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

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

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

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

Methods

(==) :: DatumCode xss ast a -> DatumCode xss ast a -> Bool

(/=) :: DatumCode xss ast a -> DatumCode xss ast a -> Bool

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

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

Constructors

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

Done :: DatumStruct '[] abt a

Instances

Traversable11 Hakaru Hakaru (DatumStruct xs)

Methods

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

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

Functor11 Hakaru Hakaru (DatumStruct xs)

Methods

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

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

Methods

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

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

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

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

Methods

(==) :: DatumStruct xs ast a -> DatumStruct xs ast a -> Bool

(/=) :: DatumStruct xs ast a -> DatumStruct xs ast a -> Bool

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

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

Constructors

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

Ident :: !(ast a) -> DatumFun I ast a

Instances

Traversable11 Hakaru Hakaru (DatumFun x)

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

Functor11 Hakaru Hakaru (DatumFun x)

Methods

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

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

Methods

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

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

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

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

Methods

(==) :: DatumFun x ast a -> DatumFun x ast a -> Bool

(/=) :: DatumFun x ast a -> DatumFun x ast a -> Bool

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

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

dFalse :: 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)

Variants which allow explicit type passing.

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)

Pattern constructors

data Branch a abt b

Constructors

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

Instances

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

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

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

ABT Hakaru Term abt => Pretty (Branch a abt)

Methods

prettyPrec_ :: Int -> Branch a abt a -> Docs

Eq2 Hakaru [Hakaru] abt => Eq (Branch a abt b)

Methods

(==) :: Branch a abt b -> Branch a abt b -> Bool

(/=) :: Branch a abt b -> Branch a abt b -> Bool

Show2 Hakaru [Hakaru] abt => Show (Branch a abt b)

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

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

Eq1 Hakaru (Pattern vars)

Methods

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

Show1 Hakaru (Pattern vars)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Eq2 Hakaru [Hakaru] Pattern

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

Pretty (Pattern xs)

Methods

prettyPrec_ :: Int -> Pattern xs a -> Docs

Eq (Pattern vars a)

Methods

(==) :: Pattern vars a -> Pattern vars a -> Bool

(/=) :: Pattern vars a -> Pattern vars a -> Bool

Show (Pattern vars a)

Methods

showsPrec :: Int -> Pattern vars a -> ShowS

show :: Pattern vars a -> String

showList :: [Pattern vars a] -> ShowS

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

Constructors

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

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

Instances

Eq2 Hakaru [Hakaru] (PDatumCode xss)

Methods

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

Show2 Hakaru [Hakaru] (PDatumCode xss)

Methods

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

show2 :: a i j -> String

Eq1 Hakaru (PDatumCode xss vars)

Methods

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

Show1 Hakaru (PDatumCode xss vars)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Eq (PDatumCode xss vars a)

Methods

(==) :: PDatumCode xss vars a -> PDatumCode xss vars a -> Bool

(/=) :: PDatumCode xss vars a -> PDatumCode xss vars a -> Bool

Show (PDatumCode xss vars a)

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

Constructors

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

PDone :: PDatumStruct '[] '[] a

Instances

Eq2 Hakaru [Hakaru] (PDatumStruct xs)

Methods

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

Show2 Hakaru [Hakaru] (PDatumStruct xs)

Methods

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

show2 :: a i j -> String

Eq1 Hakaru (PDatumStruct xs vars)

Methods

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

Show1 Hakaru (PDatumStruct xs vars)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Eq (PDatumStruct xs vars a)

Methods

(==) :: PDatumStruct xs vars a -> PDatumStruct xs vars a -> Bool

(/=) :: PDatumStruct xs vars a -> PDatumStruct xs vars a -> Bool

Show (PDatumStruct xs vars a)

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

Constructors

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

PIdent :: !(Pattern vars a) -> PDatumFun I vars a

Instances

Eq2 Hakaru [Hakaru] (PDatumFun x)

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

Eq1 Hakaru (PDatumFun x vars)

Methods

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

Show1 Hakaru (PDatumFun x vars)

Methods

showsPrec1 :: Int -> a i -> ShowS

show1 :: a i -> String

Eq (PDatumFun x vars a)

Methods

(==) :: PDatumFun x vars a -> PDatumFun x vars a -> Bool

(/=) :: PDatumFun x vars a -> PDatumFun x vars a -> Bool

Show (PDatumFun x vars a)

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

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)

Generalized branches

data GBranch a r

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

Constructors

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

Instances

Functor (GBranch a)

Methods

fmap :: (a -> b) -> GBranch a a -> GBranch a b

(<$) :: a -> GBranch a b -> GBranch a a

Foldable (GBranch a)

Methods

fold :: Monoid m => GBranch a m -> m

foldMap :: Monoid m => (a -> m) -> GBranch a a -> m

foldr :: (a -> b -> b) -> b -> GBranch a a -> b

foldr' :: (a -> b -> b) -> b -> GBranch a a -> b

foldl :: (b -> a -> b) -> b -> GBranch a a -> b

foldl' :: (b -> a -> b) -> b -> GBranch a a -> b

foldr1 :: (a -> a -> a) -> GBranch a a -> a

foldl1 :: (a -> a -> a) -> GBranch a a -> a

toList :: GBranch a a -> [a]

null :: GBranch a a -> Bool

length :: GBranch a a -> Int

elem :: Eq a => a -> GBranch a a -> Bool

maximum :: Ord a => GBranch a a -> a

minimum :: Ord a => GBranch a a -> a

sum :: Num a => GBranch a a -> a

product :: Num a => GBranch a a -> a

Traversable (GBranch a)

Methods

traverse :: Applicative f => (a -> f b) -> GBranch a a -> f (GBranch a b)

sequenceA :: Applicative f => GBranch a (f a) -> f (GBranch a a)

mapM :: Monad m => (a -> m b) -> GBranch a a -> m (GBranch a b)

sequence :: Monad m => GBranch a (m a) -> m (GBranch a a)