Type.hs

{-# LANGUAGE TypeFamilies, FlexibleContexts, TypeOperators,
  ScopedTypeVariables, UndecidableInstances, FlexibleInstances #-}

{-# LANGUAGE MultiParamTypeClasses, QuasiQuotes, GADTs #-}

{- |

Module      :  Type.Yoko.Type
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

Some fundamental types central to @yoko@.

-}

module Type.Yoko.Type
  (qK, Proxy(Proxy), module Type.Yoko.Type, module Type.Spine.Stage0,
   module Type.Booleans, IsEQ, Compare, EqT(..), (:=:)(..)) where

import Data.Proxy (Proxy(..))

import Type.Spine
import Type.Spine.Stage0 (KS, KTSS)
import Type.Serialize

import Data.Proxy.TH (qProxy)
import Type.Booleans
--import Polarity
import Type.Ord.SpineSerialize (IsEQ, Compare)

import Data.Type.Equality



qP = qProxy



-- | The @Med@ type family encodes the behavior of recursion mediators.
type family Med m a
-- | @type instance Med IdM a = a@.
data IdM = IdM; type instance Med IdM a = a




-- | The @Wrapper@ class is used to make term-level programming newtypes a
-- little more lightweight from the user perspective.
class Wrapper f where wrap :: Unwrap f a -> f a; unwrap :: f a -> Unwrap f a
type family Unwrap (f :: * -> *) a



-- | The @Pred@ type family realizes type-level predicates (over types) that
-- yield a type-level Boolean: either 'True' or 'False'. Predicates are often
-- universes.
type family Pred (p :: * -> *) a

type instance Pred ((:=:) a) b = IsEQ (Compare a b)





derive n = do
  d <- spineType n
  (d ++) `fmap` serializeTypeAsHash n





-- | Composition of @* -> *@ types.
newtype (f :. g) a = Compose (f (g a))
type instance Unwrap (f :. g) a = f (g a)
instance Wrapper (f :. g) where wrap = Compose; unwrap (Compose x) = x

-- | Explicitly takes the inner type as a proxy.
composeWith :: [qProxy|g :: *->*|] -> f (g a) -> (f :. g) a
composeWith _ = Compose