{-# LANGUAGE DataKinds
, PolyKinds
, TypeOperators
, TypeFamilies
, StandaloneDeriving
, DeriveDataTypeable
, ScopedTypeVariables
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Types.DataKind
(
Hakaru(..)
, HakaruFun(..)
, HakaruCon(..)
, Symbol
, Code
, HData'
, HBool, HUnit, HPair, HEither, HList, HMaybe
) where
import Data.Typeable (Typeable)
import GHC.TypeLits (Symbol)
infixr 0 :->
data Hakaru
= HNat
| HInt
| HProb
| HReal
| HMeasure !Hakaru
| HArray !Hakaru
| !Hakaru :-> !Hakaru
| HData !HakaruCon [[HakaruFun]]
deriving instance Typeable 'HNat
deriving instance Typeable 'HInt
deriving instance Typeable 'HProb
deriving instance Typeable 'HReal
deriving instance Typeable 'HMeasure
deriving instance Typeable 'HArray
deriving instance Typeable '(:->)
deriving instance Typeable 'HData
----------------------------------------------------------------
-- | 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.
data HakaruFun = I | K !Hakaru
deriving instance Typeable 'I
deriving instance Typeable 'K
----------------------------------------------------------------
-- | 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\".
data HakaruCon = TyCon !Symbol | HakaruCon :@ Hakaru
infixl 0 :@
deriving instance Typeable 'TyCon
deriving instance Typeable '(:@)
-- | 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 family Code (a :: HakaruCon) :: [[HakaruFun]]
type instance Code ('TyCon "Bool") = '[ '[], '[] ]
type instance Code ('TyCon "Unit") = '[ '[] ]
type instance Code ('TyCon "Maybe" ':@ a) = '[ '[] , '[ 'K a ] ]
type instance Code ('TyCon "List" ':@ a) = '[ '[] , '[ 'K a, 'I ] ]
type instance Code ('TyCon "Pair" ':@ a ':@ b) = '[ '[ 'K a, 'K b ] ]
type instance Code ('TyCon "Either" ':@ a ':@ b) = '[ '[ 'K a ], '[ 'K b ] ]
-- | 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.
type HData' t = 'HData t (Code t)
{-
>:kind! forall a b . HData' (TyCon "Pair" :@ a :@ b)
forall a b . HData' (TyCon "Pair" :@ a :@ b) :: Hakaru
= forall (a :: Hakaru) (b :: Hakaru).
'HData (('TyCon "Pair" ':@ a) ':@ b) '['['K a, 'K b]]
type HBool = HData' (TyCon "Bool")
type HUnit = HData' (TyCon "Unit")
type HPair a b = HData' (TyCon "Pair" :@ a :@ b)
type HEither a b = HData' (TyCon "Either" :@ a :@ b)
type HList a = HData' (TyCon "List" :@ a)
type HMaybe a = HData' (TyCon "Maybe" :@ a)
-}
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] ]
----------------------------------------------------------------
----------------------------------------------------------- fin.