{-# LANGUAGE TypeFamilies, ScopedTypeVariables, QuasiQuotes, Rank2Types, GADTs, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, EmptyDataDecls, TypeOperators #-} {-# LANGUAGE TemplateHaskell #-} {- | Module : Type.Yoko.BTree Copyright : (c) The University of Kansas 2011 License : BSD3 Maintainer : nicolas.frisby@gmail.com Stability : experimental Portability : see LANGUAGE pragmas (... GHC) Operators for the type-sums from "Type.Yoko.Sum". -} module Type.Yoko.BTree where import Type.Yoko.Type import Type.Yoko.Universe import Type.Yoko.Natural import Data.Yoko.Core import Type.Yoko.Sum -- | @Inu t@ is a universe of type-sums containing @t@. type Inu t = Exists ((:=:) t) -- | @Uni ts@ is a universe containing the types in the type-sum @ts@. newtype Uni ts t = Uni (Inu t ts) instance (ts ::: Inu t) => t ::: Uni ts where inhabits = Uni inhabits type instance Pred (Uni ts) t = Elem t ts instance (ts ::: TSum) => EqT (Uni ts) where eqT (Uni u) (Uni v) = w u v where w :: forall ts a b. Inu a ts -> Inu b ts -> Maybe (a :=: b) w (Here Refl) (Here Refl) = Just Refl w (OnLeft u) (OnLeft v) = w u v w (OnRight u) (OnRight v) = w u v w _ _ = Nothing -- | A @Uni ts t@ value can also be understood in terms of more primitive -- universes, 'VoidU', @':=:'@ and @':||'@ for 'V', 'N', and @':+'@, -- respectively. type family PrimUni ts :: * -> * type instance PrimUni V = VoidU type instance PrimUni (N t) = (:=:) t type instance PrimUni (ts :+ us) = PrimUni ts :|| PrimUni us primUni :: Uni ts t -> PrimUni ts t primUni (Uni u) = w u where w :: Inu t ts -> PrimUni ts t w (Here Refl) = Refl w (OnLeft u) = LeftD $ w u w (OnRight v) = RightD $ w v primUni1 :: Uni (ts :+ us) t -> (Uni ts :|| Uni us) t primUni1 (Uni (OnLeft u)) = LeftD $ Uni u primUni1 (Uni (OnRight v)) = RightD $ Uni v -- | Finite universes can be represented as type-sums. type family Inhabitants u class (Inhabitants u ::: TSum) => Finite u where toUni :: u t -> Uni (Inhabitants u) t -- | @fromUni@ sometimes requires a stronger context than does @toUni@, so we -- separate the two methods. class Finite u => Etinif u where fromUni :: Uni (Inhabitants u) t -> u t -- | Any finite universe can be used to determine type equality. eqTFin :: (Inhabitants u ~ Inhabitants v, Finite u, Finite v ) => u a -> v b -> Maybe (a :=: b) eqTFin x y = eqT (toUni x) (toUni y) type instance Inhabitants (Uni ts) = ts instance (ts ::: TSum) => Finite (Uni ts) where toUni = id instance Finite (Uni ts) => Etinif (Uni ts) where fromUni = id -- | @Norm@ uses @NormW@ to remove duplicates from (i.e. /normalize/) a -- type-sum. type family Norm c type instance Norm V = V type instance Norm (N t) = N t type instance Norm (ts :+ us) = NormW (ts :+ us) V -- | @NormW@ combines two type-sums into a right-associated type-sum containing -- no duplicates. type family NormW c acc type instance NormW V acc = acc type instance NormW (N t) acc = If (Elem t acc) acc (N t :+ acc) type instance NormW (ts :+ us) acc = NormW ts (NormW us acc) -- | @Each ts f@ provides a @'NT' t f@ for each @t@ in the type-sum @ts@. type Each ts = NT (Uni ts) none :: String -> Each V f none s = NT $ error $ "TypeBTree.none: " ++ s one_ :: [qP|f :: *->*|] -> Unwrap f t -> Each (N t) f one_ p x = firstNT primUni $ constNT_ p x one :: Unwrap f t -> Each (N t) f one = one_ Proxy oneF :: Wrapper f => f t -> Each (N t) f oneF x = firstNT primUni $ constNTF x infixr 6 |||, .|. both, (|||) :: Each ts f -> Each us f -> Each (ts :+ us) f both f g = firstNT primUni1 $ orNT f g; (|||) = both infixl 5 ||.; infixr 5 .|| (.|.) :: Wrapper f => Unwrap f t -> Unwrap f s -> Each (N t :+ N s) f (||.) :: Wrapper f => Each ts f -> Unwrap f t -> Each (ts :+ N t) f (.||) :: Wrapper f => Unwrap f t -> Each ts f -> Each (N t :+ ts) f f .|. g = one f ||| one g; f ||. g = f ||| one g; f .|| g = one f ||| g -- | @each@ is the principal means of defining an @Each@ value. each :: forall u ts f. (ts ::: All u) => [qP|u :: *->*|] -> (forall a. u a -> Unwrap f a) -> Each ts f each _ = \fs -> w inhabits fs where w :: forall ts. All u ts -> (forall a. (a ::: u) => u a -> Unwrap f a) -> Each ts f w SumV _ = none "TypeBTree.each" w (SumN u) fns = one $ fns u w (SumS c d) fns = w c fns `both` w d fns eachF :: forall u ts f. (Wrapper f, ts ::: All u) => [qP|u :: *->*|] -> (forall a. u a -> f a) -> Each ts f eachF p f = each p (unwrap . f) eachF_ :: forall f ts. (Wrapper f, ts ::: All NoneD) => (forall a. f a) -> Each ts f eachF_ f = eachF Proxy ((\NoneD -> f) :: forall a. NoneD a -> f a) -- | Just a specialization: @prjEach x f = 'appNT' f x@. prjEach :: Uni ts t -> Each ts f -> Unwrap f t prjEach x f = appNT f x prjEachF :: Wrapper f => Uni ts t -> Each ts f -> f t prjEachF = (wrap .) . prjEach -- | @eachOrNT fs gs@ builds an 'NT' that uses @fs@ for as many types in the -- universe @v@ as possible, and uses @gs@ for the rest. It's an extension of -- 'orNT' to @Each@. eachOrNT :: forall u v f w. (Inhabitants v ::: All (u :|| w), Finite v) => NT u f -> NT w f -> NT v f eachOrNT fs dflt = firstNT toUni $ each Proxy $ appNT $ orNT fs dflt