# Data representation

Data types are stored using a sum of product representation.
They can be found in `Language.Hakaru.Syntax.Datum`

.

```
-- 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.
data Datum :: (Hakaru -> *) -> Hakaru -> * where
Datum
:: {-# UNPACK #-} !Text
-> !(Sing (HData' t))
-> !(DatumCode (Code t) ast (HData' t))
-> Datum ast (HData' t)
-- | 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.
data DatumCode :: [[HakaruFun]] -> (Hakaru -> *) -> Hakaru -> * where
-- Skip rightwards along the sum.
Inr :: !(DatumCode xss abt a) -> DatumCode (xs ': xss) abt a
-- Inject into the sum.
Inl :: !(DatumStruct xs abt a) -> DatumCode (xs ': xss) abt a
data DatumStruct :: [HakaruFun] -> (Hakaru -> *) -> Hakaru -> * where
-- BUG: haddock doesn't like annotations on GADT constructors
-- <https://github.com/hakaru-dev/hakaru/issues/6>
-- Combine components of the product. (\"et\" means \"and\" in Latin)
Et :: !(DatumFun x abt a)
-> !(DatumStruct xs abt a)
-> DatumStruct (x ': xs) abt a
-- Close off the product.
Done :: DatumStruct '[] abt a
data DatumFun :: HakaruFun -> (Hakaru -> *) -> Hakaru -> * where
-- Hit a leaf which isn't a recursive component of the datatype.
Konst :: !(ast b) -> DatumFun ('K b) ast a
-- Hit a leaf which is a recursive component of the datatype.
Ident :: !(ast a) -> DatumFun 'I ast a
```

In Hakaru we have implemented Bool, Pair, Either, Maybe, and List.