{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances, EmptyDataDecls #-}

{-# LANGUAGE TemplateHaskell #-}

{- |

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

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

The core structural types; \"sum of products\" and such.

-}

module Data.Yoko.Core where

import Type.Yoko.Type (derive)

--import Polarity



-- | Structural representations (e.g. "Data.Yoko.Generic"'s 'RM') of a @*@ type
-- can be derived as a data family indexed by the core representation (@Rep@)
-- of that type.
type family Rep a



-- | void
data V
-- | unit
data U = U
-- | a dependency
newtype D a = D a
-- | a recursive occurrence
newtype R t = R t
-- | argument to a @* -> *@
newtype F f c = F (f c)
-- | arguments to a @* -> * -> *@
newtype FF ff c d = FF (ff c d)
-- | meta information
newtype M i c = M c

-- | a named intermediate (user hook); crucially: @type instance Rep (N t) =
-- Rep t@.
newtype N t = N t

type instance Rep (N t) = Rep t   -- this is the crucial meaning of N



concat `fmap` mapM derive [''V, ''U, ''D, ''R, ''F, ''FF, ''M, ''N]



infixr 6 :*
type (:*) = FF (,)





{-
type instance Polarity ([qK|*->*->*|] M) (ki :* kt :* U) = Neutral
type instance Polarity ([qK|*->*|] (M i)) (kt :* U) = Pos

type instance Polarity ([qK|*->*|] R) (ka :* U) = Pos

type instance Polarity ([qK|(*->*)->*->*|] F) (kf :* kt :* U) = Pos
type instance Polarity ([qK|*->*|] (F f)) (kt :* U) =
  Polarity ([qK|*->*|] f) (kt :* U)

type instance Polarity ([qK|(*->*->*)->*->*->*|] FF) (kff :* kt :* ks :* U) = Pos
type instance Polarity ([qK|*->*->*|] (FF ff)) (kt :* ks :* U) =
  Polarity ([qK|*->*->*|] ff) (kt :* ks :* U)
type instance Polarity ([qK|*->*|] (FF ff t)) (ks :* U) =
  Polarity ([qK|*->*|] (ff t)) (ks :* U)
-}