module Type.Yoko.Sum ((:+), All(..), TSum, Exists(..), Elem) where
import Type.Yoko.Type
import Type.Yoko.Universe
import Data.Yoko.CoreTypes
infixr 5 :+
data t :+ s
data All u c where
SumV :: All u V
SumN :: (t ::: u) => u t -> All u (N t)
SumS :: All u c -> All u d -> All u (c :+ d)
instance V ::: All u where inhabits = SumV
instance (t ::: u) => N t ::: All u where inhabits = SumN inhabits
instance (c ::: All u, d ::: All u) => (c :+ d) ::: All u where
inhabits = SumS inhabits inhabits
type TSum = All NoneU
data Exists p c where
Here :: p t -> Exists p (N t)
OnLeft :: Exists p c -> Exists p (c :+ d)
OnRight :: Exists p d -> Exists p (c :+ d)
data Nothing; data Just path
type family IsJust a
type instance IsJust Nothing = False
type instance IsJust (Just path) = True
type family Combine l r
type instance Combine Nothing Nothing = Nothing
type instance Combine Nothing (Just x) = Just (OnRight x)
type instance Combine (Just x) r = Just (OnLeft x)
data Here
data OnLeft x
data OnRight x
type Elem t ts = IsJust (Find ((:=:) t) ts)
type family Find (pred :: * -> *) c
type instance Find p (N t) = If (Pred p t) (Just Here) Nothing
type instance Find p (c :+ d) = Combine (Find p c) (Find p d)
type instance Find p V = Nothing
instance (Just path ~ Find p c, c ::: Exists p :? path) => c ::: Exists p where
inhabits = inhabits_ [qP|path|]
instance (t ::: p) => N t ::: Exists p :? Here where
inhabits = Anno $ Here inhabits
instance (c ::: Exists p :? path) => (c :+ d) ::: Exists p :? OnLeft path where
inhabits = Anno $ OnLeft (inhabits_ [qP|path|])
instance (d ::: Exists p :? path) => (c :+ d) ::: Exists p :? OnRight path where
inhabits = Anno $ OnRight (inhabits_ [qP|path|])