module Data.Type.Subset
( module Data.Type.Subset
, module Exports
) where
import Type.Class.Higher
import Type.Class.Known
import Type.Class.Witness
import Type.Family.List
import Data.Type.Index
import Data.Type.Length
import Data.Type.Product as Exports (Prod(..))
import Data.Type.Product (index)
import Data.Type.Sum (Sum(..),prj)
import Control.Applicative ((<|>))
type Subset as = Prod (Index as)
subNil :: Subset Ø as -> (as :~: Ø)
subNil = \case
Ø -> Refl
x :< _ -> ixNil x
type as ⊆ bs = Every (Elem bs) as
infix 4 ⊆
subRefl :: Known Length as
=> Subset as as
subRefl = go known
where
go :: Length xs -> Subset xs xs
go = \case
LZ -> Ø
LS l -> IZ :< map1 IS (go l)
subTrans :: Subset as bs -> Subset bs cs -> Subset as cs
subTrans s = map1 $ subIx s
subProd :: Subset as bs -> Prod f as -> Prod f bs
subProd = \case
Ø -> pure Ø
x :< s -> (:<) <$> index x <*> subProd s
subSum :: Subset as bs -> Sum f as -> Maybe (Sum f bs)
subSum = \case
Ø -> pure Nothing
x :< s -> \t -> (InL <$> (prj t \\ x))
<|> (InR <$> subSum s t)
subIx :: Subset as bs -> Index bs x -> Index as x
subIx = \case
Ø -> ixNil
x :< s -> \case
IZ -> x
IS y -> subIx s y
subExt :: Known Length as => (forall x. Index as x -> Index bs x) -> Subset bs as
subExt f = subExtBy f known
subExtBy :: (forall x. Index as x -> Index bs x) -> Length as -> Subset bs as
subExtBy f = \case
LZ -> Ø
LS l -> f IZ :< subExtBy (f . IS) l