Universe.hs

{-# LANGUAGE MultiParamTypeClasses, QuasiQuotes, TypeFamilies, TypeOperators,
  FlexibleContexts, ScopedTypeVariables, FlexibleInstances,
  UndecidableInstances, GADTs, Rank2Types, EmptyDataDecls #-}

{- |

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

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

Type universes.

-}

module Type.Yoko.Universe where

import Type.Yoko.Type

infix 0 :::
-- | A /universe/ determines a set of types; /open/ or /closed/. @(:::)@ is
-- comparable to the @Sat@ class (e.g. from @SYB3@).
class a ::: u where inhabits :: u a



-- | @(:?)@ helps us write /guarded/ @(:::)@ instances (see
-- <http://hackage.haskell.org/trac/ghc/ticket/5590>)
infix 1 :?
data (u :? anno) a = Anno (u a)


-- | For use with @(:::)@ instances that use @(:?)@.
inhabits_ :: forall a u anno. (a ::: u :? anno) => [qP|anno|] -> u a
inhabits_ _ = i where Anno i = inhabits :: (u :? anno) a

-- | Sometimes it's helpful to specify which @t@ must be in the universe.
inhabitsFor :: (t ::: u) => [qP|t|] -> u t
inhabitsFor _ = inhabits



-- | The universe of all types; it has /no/ contraints.
data NoneU a = NoneU
instance a ::: NoneU where inhabits = NoneU

type Both = (:&&)
infixr 3 :&&
-- | Universe product.
data (u :&& v) a where (:&&) :: (a ::: u, a ::: v) => {fstU :: u a, sndU :: v a} -> (u :&& v) a
instance (a ::: u, a ::: v) => a ::: u :&& v where
  inhabits = inhabits :&& inhabits

type instance Pred (p :&& q) a = And (Pred p a) (Pred q a)



instance (a ~ b) => b ::: (:=:) a where inhabits = Refl


infixr 2 :||
-- | Universe sum.
data (u :|| v) a where
  LeftU  :: u a -> (u :|| v) a
  RightU :: v a -> (u :|| v) a

instance (anno ~ Pred u a, a ::: u :|| v :? anno) => a ::: u :|| v where
  inhabits = inhabits_ [qP|anno|]
instance (True  ~ Pred u a, a ::: u) => a ::: u :|| v :? True where
  inhabits = Anno $ LeftU inhabits
instance (False ~ Pred u a, a ::: v) => a ::: u :|| v :? False where
  inhabits = Anno $ RightU inhabits


type instance Pred (u :|| v) t = Or (Pred u t) (Pred v t)



-- | The empty universe.
data VoidU t -- the empty universe



instance (f t ::: u) => t ::: (u :. f) where inhabits = Compose inhabits