{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}

module Base where

-------------------------------------------------------------------------------
-- structure types
-------------------------------------------------------------------------------

infixr 5 :+:
infix  6 :::
infixr 7 :*:

data Id :: * -> (* -> *) -> (* -> *) -> * -> * where
  Id :: Ix l xi => r xi -> Id xi l r ix

unId :: Id xi l r ix -> r xi
unId (Id x) = x

data I a = I {unI :: a}

data K a       (l :: * -> *) (r :: * -> *) ix = K {unK :: a}
data (f :+: g) (l :: * -> *) (r :: * -> *) ix = L (f l r ix) | R (g l r ix)
data (f :*: g) (l :: * -> *) (r :: * -> *) ix = f l r ix :*: g l r ix

data (:::) :: ((* -> *) -> (* -> *) -> * -> *) -> * -> (* -> *) -> (* -> *) -> * -> * where
  Tag {unTag :: f l r ix} :: (f ::: ix) l r ix

-------------------------------------------------------------------------------
-- indexed families, generically
-------------------------------------------------------------------------------

type family PF l :: (* -> *) -> (* -> *) -> * -> *

type Str l = (PF l) l

class Ix l ix where
  ix   :: l ix
  from :: ix -> Str l I ix
  to   :: Str l I ix -> ix