Copyright	Copyright (C) 2015 Kyle Carter
License	BSD3
Maintainer	Kyle Carter <kylcarte@indiana.edu>
Stability	experimental
Portability	RankNTypes
Safe Haskell	None
Language	Haskell2010

Data.Type.Difference

Description

A singleton-esque type for representing the removal of a subset of a type level list.

Documentation

data Difference :: [k] -> [k] -> [k] -> * where Source #

Constructors

ØD :: Difference as Ø as
(:-) :: !(Remove bs a cs) -> !(Difference cs as ds) -> Difference bs (a :< as) ds infixr 5

Instances

Witness ØC (WithoutAll k as bs cs) (Difference k as bs cs) Source #
Associated Types type WitnessC (ØC :: Constraint) (WithoutAll k as bs cs :: Constraint) (Difference k as bs cs) :: Constraint Source # Methods (\\) :: ØC => (WithoutAll k as bs cs -> r) -> Difference k as bs cs -> r Source #
TestEquality [k] (Difference k as bs) Source #
Methods testEquality :: f a -> f b -> Maybe ((Difference k as bs :~: a) b) #
WithoutAll k as bs cs => Known [k] (Difference k as bs) cs Source #
Associated Types type KnownC (Difference k as bs) (cs :: Difference k as bs -> *) (a :: Difference k as bs) :: Constraint Source # Methods known :: cs a Source #
type WitnessC ØC (WithoutAll k as bs cs) (Difference k as bs cs) Source #
type WitnessC ØC (WithoutAll k as bs cs) (Difference k as bs cs) = ØC
type KnownC [k] (Difference k as bs) cs Source #
type KnownC [k] (Difference k as bs) cs = WithoutAll k as bs cs

elimDifference :: (forall xs. p xs Ø xs) -> (forall x ws xs ys zs. Remove xs x ys -> Difference ys ws zs -> p ys ws zs -> p xs (x :< ws) zs) -> Difference as bs cs -> p as bs cs Source #

diffProd :: Difference as bs cs -> Prod f as -> (Prod f bs, Prod f cs) Source #

diffSum :: Difference as bs cs -> Sum f as -> Either (Sum f bs) (Sum f cs) Source #

class WithoutAll as bs cs | as bs -> cs where Source #

Minimal complete definition

Methods

Instances

(~) [k] cs as => WithoutAll k as (Ø k) cs Source #
Methods withoutAll :: Difference as (Ø k) cs cs Source #
(Without a as b cs, WithoutAll a cs bs ds) => WithoutAll a as ((:<) a b bs) ds Source #
Methods withoutAll :: Difference as ((a :< b) bs) ds cs Source #
Witness ØC (WithoutAll k as bs cs) (Difference k as bs cs) Source #
Associated Types type WitnessC (ØC :: Constraint) (WithoutAll k as bs cs :: Constraint) (Difference k as bs cs) :: Constraint Source # Methods (\\) :: ØC => (WithoutAll k as bs cs -> r) -> Difference k as bs cs -> r Source #
type WitnessC ØC (WithoutAll k as bs cs) (Difference k as bs cs) Source #
type WitnessC ØC (WithoutAll k as bs cs) (Difference k as bs cs) = ØC