type-combinators-0.2.4.3: A collection of data types for type-level programming

CopyrightCopyright (C) 2015 Kyle Carter
LicenseBSD3
MaintainerKyle Carter <kylcarte@indiana.edu>
Stabilityexperimental
PortabilityRankNTypes
Safe HaskellNone
LanguageHaskell2010

Data.Type.Subset

Description

A singleton-esque type for representing subsets of a type level list.

Documentation

type Subset as = Prod (Index as) Source #

subNil :: Subset Ø as -> as :~: Ø Source #

type (⊆) as bs = Every (Elem bs) as infix 4 Source #

subRefl :: Known Length as => Subset as as Source #

subTrans :: Subset as bs -> Subset bs cs -> Subset as cs Source #

subProd :: Subset as bs -> Prod f as -> Prod f bs Source #

subSum :: Subset as bs -> Sum f as -> Maybe (Sum f bs) Source #

subIx :: Subset as bs -> Index bs x -> Index as x Source #

subExt :: Known Length as => (forall x. Index as x -> Index bs x) -> Subset bs as Source #

subExtBy :: (forall x. Index as x -> Index bs x) -> Length as -> Subset bs as Source #