module Type.Yoko.Universe where
import Type.Yoko.Type
infix 0 :::
class a ::: u where inhabits :: u a
infix 1 :?
data (u :? anno) a = Anno (u a)
inhabits_ :: forall a u anno. (a ::: u :? anno) => [qP|anno|] -> u a
inhabits_ _ = i where Anno i = inhabits :: (u :? anno) a
inhabitsFor :: (t ::: u) => [qP|t|] -> u t
inhabitsFor _ = inhabits
data NoneU a = NoneU
instance a ::: NoneU where inhabits = NoneU
type Both = (:&&)
infixr 3 :&&
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 :||
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)
data VoidU t
instance (f t ::: u) => t ::: (u :. f) where inhabits = Compose inhabits