universe-dependent-sum-1.1: Universe instances for types from dependent-sum

Safe HaskellSafe
LanguageHaskell2010

Data.Universe.Some

Contents

Synopsis

Documentation

class UniverseSome f where Source #

Auxiliary class to power Universe (Some f) instance. (There are no good reasons to use FlexibleInstances).

Laws are induced via Universe (Some f) instance. For example:

elem x universe ==> elem (Some f) universeSome

As GEq cannot be written for phantom Functors, e.g. Const or Proxy, they cannot have UniverseSome instance either.

Methods

universeSome :: [Some f] Source #

Instances
UniverseSome ((:~:) a) Source # 
Instance details

Defined in Data.Universe.Some

Methods

universeSome :: [Some ((:~:) a)] Source #

(UniverseSome f, UniverseSome g) => UniverseSome (Sum f g) Source # 
Instance details

Defined in Data.Universe.Some

Methods

universeSome :: [Some (Sum f g)] Source #

class UniverseSome f => FiniteSome f where Source #

Minimal complete definition

Nothing

Methods

universeFSome :: [Some f] Source #

cardinalitySome :: Tagged (Some f) Natural Source #

Instances
FiniteSome ((:~:) a) Source # 
Instance details

Defined in Data.Universe.Some

Methods

universeFSome :: [Some ((:~:) a)] Source #

cardinalitySome :: Tagged (Some ((:~:) a)) Natural Source #

(FiniteSome f, FiniteSome g) => FiniteSome (Sum f g) Source # 
Instance details

Defined in Data.Universe.Some

Methods

universeFSome :: [Some (Sum f g)] Source #

cardinalitySome :: Tagged (Some (Sum f g)) Natural Source #

Orphan instances

UniverseSome f => Universe (Some f) Source # 
Instance details

Methods

universe :: [Some f] #

FiniteSome f => Finite (Some f) Source # 
Instance details

Methods

universeF :: [Some f] #

cardinality :: Tagged (Some f) Natural #