Data.Universe.Some

Documentation

class UniverseSome f where

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]

Instances

UniverseSome ((:~:) a)

Defined in Data.Universe.Some

Methods

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

(UniverseSome f, UniverseSome g) => UniverseSome (Sum f g)

Defined in Data.Universe.Some

Methods

universeSome :: [Some (Sum f g)]

class UniverseSome f => FiniteSome f where

Minimal complete definition

Nothing

Methods

universeFSome :: [Some f]

cardinalitySome :: Tagged (Some f) Natural

Instances

FiniteSome ((:~:) a)

Defined in Data.Universe.Some

Methods

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

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

(FiniteSome f, FiniteSome g) => FiniteSome (Sum f g)

Defined in Data.Universe.Some

Methods

universeFSome :: [Some (Sum f g)]

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

Orphan instances

UniverseSome f => Universe (Some f)

Methods

universe :: [Some f]

FiniteSome f => Finite (Some f)

Methods

universeF :: [Some f]

cardinality :: Tagged (Some f) Natural