cardano-data-1.2.3.0: Specialized data for Cardano project
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Universe

Description

The idea is to create a world of Haskell types, called a Universe. Then to define a 'class' whose methods are only applicable to that set of types. We define a closed set by defining an indexed type constructor Rep. If (Singleton Rep), then it must be that every value of type (Rep t) has exactly 0 or 1 inhabitants. (Rep t) has exactly 1 inhabitant if t is in the universe, and 0 inhabitants if it is not in the universe. A closely related class is (Indexed s t). We would like a total ordering on (t i) and (t j), where the indices, i and j, are different. We do this by ensuring every value of type (t i) has a unique Shape, and that the type Shape has a total order. Every closed singleton can be totally ordered this way. Other indexed types are used to make well-type terms. I.e. Indexed s t => Exp t, denotes a Haskell data type Exp, related to the type t. Note, unlike singletons, there may not be a unique value of type (Exp t), but there may be a unique Shape for every value.

Synopsis

Documentation

class Shaped t rep where Source #

For some indexed types, we can assign a unique Shape to each type, using: shape :: t i -> Shape s (where s is some Singleton type) the class (Shaped t s) means we can assign a unique Shape to each value of type (t i). Not quite as strong as having a unique inhabitant. Every closed singleton type can be shaped, and many other indexed types can be shaped as well.

Methods

shape ∷ t i → Shape rep Source #

class Singleton t where Source #

Given (Singleton T), a value of type (T i) has exactly 0 or 1 inhabitants, so we can compare the structure of the type to get proofs that the indexes (i and j) are the same type, using testEql, at runtime. cmpIndex, it is like compare except we can have two different indexes (a and b).

Methods

testEql ∷ t i → t j → Maybe (i :~: j) Source #

cmpIndex ∷ t a → t b → Ordering Source #

Instances

Instances details
Singleton (TypeRep ∷ k → Type) Source # 
Instance details

Defined in Data.Universe

Methods

testEql ∷ ∀ (i ∷ k0) (j ∷ k0). TypeRep i → TypeRep j → Maybe (i :~: j) Source #

cmpIndex ∷ ∀ (a ∷ k0) (b ∷ k0). TypeRep a → TypeRep b → Ordering Source #

class Singleton rep ⇒ Universe rep t where Source #

A minimal class of operations defined on the universe described by rep . Feel free to make your own Universe classes with additional methods

Methods

repOf ∷ rep t Source #

data Any t where Source #

Hide the index for any indexed type t

Constructors

Any ∷ t i → Any t 

Instances

Instances details
(∀ (i ∷ k). Show (t i)) ⇒ Show (Any t) Source # 
Instance details

Defined in Data.Universe

Methods

showsPrecIntAny t → ShowS Source #

showAny t → String Source #

showList ∷ [Any t] → ShowS Source #

data Some t where Source #

Hide the index for a singleton type t

Constructors

SomeSingleton t ⇒ t i → Some t 

Instances

Instances details
Eq (Some r) Source # 
Instance details

Defined in Data.Universe

Methods

(==)Some r → Some r → Bool Source #

(/=)Some r → Some r → Bool Source #

Ord (Some r) Source # 
Instance details

Defined in Data.Universe

Methods

compareSome r → Some r → Ordering Source #

(<)Some r → Some r → Bool Source #

(<=)Some r → Some r → Bool Source #

(>)Some r → Some r → Bool Source #

(>=)Some r → Some r → Bool Source #

maxSome r → Some r → Some r Source #

minSome r → Some r → Some r Source #

data Dyn rep where Source #

Constructors

DynSingleton t ⇒ t i → i → Dyn t 

data Shape rep where Source #

Constructors

NullaryIntShape rep 
NaryInt → [Shape rep] → Shape rep 
Esc ∷ (Singleton rep, Ord t) ⇒ rep t → t → Shape rep 

Instances

Instances details
Eq (Shape rep) Source # 
Instance details

Defined in Data.Universe

Methods

(==)Shape rep → Shape rep → Bool Source #

(/=)Shape rep → Shape rep → Bool Source #

Ord (Shape rep) Source # 
Instance details

Defined in Data.Universe

Methods

compareShape rep → Shape rep → Ordering Source #

(<)Shape rep → Shape rep → Bool Source #

(<=)Shape rep → Shape rep → Bool Source #

(>)Shape rep → Shape rep → Bool Source #

(>=)Shape rep → Shape rep → Bool Source #

maxShape rep → Shape rep → Shape rep Source #

minShape rep → Shape rep → Shape rep Source #

type Eql x y = x :~: y Source #

Type synonym, so we can use ( :~: ) without TypeOperators

data (a ∷ k) :~: (b ∷ k) where infix 4 Source #

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Since: base-4.7.0.0

Constructors

Refl ∷ ∀ {k} (a ∷ k). a :~: a 

Instances

Instances details
TestEquality ((:~:) a ∷ k → Type)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

testEquality ∷ ∀ (a0 ∷ k0) (b ∷ k0). (a :~: a0) → (a :~: b) → Maybe (a0 :~: b) Source #

GCompare ((:~:) a ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gcompare ∷ ∀ (a0 ∷ k0) (b ∷ k0). (a :~: a0) → (a :~: b) → GOrdering a0 b Source #

GEq ((:~:) a ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

geq ∷ ∀ (a0 ∷ k0) (b ∷ k0). (a :~: a0) → (a :~: b) → Maybe (a0 :~: b) Source #

GRead ((:~:) a ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

greadsPrecIntGReadS ((:~:) a) Source #

GShow ((:~:) a ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gshowsPrec ∷ ∀ (a0 ∷ k0). Int → (a :~: a0) → ShowS Source #

NFData2 ((:~:)TypeTypeType)

Since: deepseq-1.4.3.0

Instance details

Defined in Control.DeepSeq

Methods

liftRnf2 ∷ (a → ()) → (b → ()) → (a :~: b) → () Source #

NFData1 ((:~:) a)

Since: deepseq-1.4.3.0

Instance details

Defined in Control.DeepSeq

Methods

liftRnf ∷ (a0 → ()) → (a :~: a0) → () Source #

a ~ b ⇒ Bounded (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

minBound ∷ a :~: b Source #

maxBound ∷ a :~: b Source #

a ~ b ⇒ Enum (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

succ ∷ (a :~: b) → a :~: b Source #

pred ∷ (a :~: b) → a :~: b Source #

toEnumInt → a :~: b Source #

fromEnum ∷ (a :~: b) → Int Source #

enumFrom ∷ (a :~: b) → [a :~: b] Source #

enumFromThen ∷ (a :~: b) → (a :~: b) → [a :~: b] Source #

enumFromTo ∷ (a :~: b) → (a :~: b) → [a :~: b] Source #

enumFromThenTo ∷ (a :~: b) → (a :~: b) → (a :~: b) → [a :~: b] Source #

a ~ b ⇒ Read (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Show (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

showsPrecInt → (a :~: b) → ShowS Source #

show ∷ (a :~: b) → String Source #

showList ∷ [a :~: b] → ShowS Source #

NFData (a :~: b)

Since: deepseq-1.4.3.0

Instance details

Defined in Control.DeepSeq

Methods

rnf ∷ (a :~: b) → () Source #

Eq (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

(==) ∷ (a :~: b) → (a :~: b) → Bool Source #

(/=) ∷ (a :~: b) → (a :~: b) → Bool Source #

Ord (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

compare ∷ (a :~: b) → (a :~: b) → Ordering Source #

(<) ∷ (a :~: b) → (a :~: b) → Bool Source #

(<=) ∷ (a :~: b) → (a :~: b) → Bool Source #

(>) ∷ (a :~: b) → (a :~: b) → Bool Source #

(>=) ∷ (a :~: b) → (a :~: b) → Bool Source #

max ∷ (a :~: b) → (a :~: b) → a :~: b Source #

min ∷ (a :~: b) → (a :~: b) → a :~: b Source #

data TypeRep (a ∷ k) Source #

A concrete representation of a (monomorphic) type. TypeRep supports reasonably efficient equality.

Instances

Instances details
TestEquality (TypeRep ∷ k → Type) 
Instance details

Defined in Data.Typeable.Internal

Methods

testEquality ∷ ∀ (a ∷ k0) (b ∷ k0). TypeRep a → TypeRep b → Maybe (a :~: b) Source #

Singleton (TypeRep ∷ k → Type) Source # 
Instance details

Defined in Data.Universe

Methods

testEql ∷ ∀ (i ∷ k0) (j ∷ k0). TypeRep i → TypeRep j → Maybe (i :~: j) Source #

cmpIndex ∷ ∀ (a ∷ k0) (b ∷ k0). TypeRep a → TypeRep b → Ordering Source #

GCompare (TypeRep ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gcompare ∷ ∀ (a ∷ k0) (b ∷ k0). TypeRep a → TypeRep b → GOrdering a b Source #

GEq (TypeRep ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

geq ∷ ∀ (a ∷ k0) (b ∷ k0). TypeRep a → TypeRep b → Maybe (a :~: b) Source #

GShow (TypeRep ∷ k → Type) 
Instance details

Defined in Data.GADT.Internal

Methods

gshowsPrec ∷ ∀ (a ∷ k0). IntTypeRep a → ShowS Source #

Show (TypeRep a) 
Instance details

Defined in Data.Typeable.Internal

Methods

showsPrecIntTypeRep a → ShowS Source #

showTypeRep a → String Source #

showList ∷ [TypeRep a] → ShowS Source #

Eq (TypeRep a)

Since: base-2.1

Instance details

Defined in Data.Typeable.Internal

Methods

(==)TypeRep a → TypeRep a → Bool Source #

(/=)TypeRep a → TypeRep a → Bool Source #

Ord (TypeRep a)

Since: base-4.4.0.0

Instance details

Defined in Data.Typeable.Internal

Methods

compareTypeRep a → TypeRep a → Ordering Source #

(<)TypeRep a → TypeRep a → Bool Source #

(<=)TypeRep a → TypeRep a → Bool Source #

(>)TypeRep a → TypeRep a → Bool Source #

(>=)TypeRep a → TypeRep a → Bool Source #

maxTypeRep a → TypeRep a → TypeRep a Source #

minTypeRep a → TypeRep a → TypeRep a Source #

Hashable (TypeRep a) 
Instance details

Defined in Data.Hashable.Class

Methods

hashWithSaltIntTypeRep a → Int Source #

hashTypeRep a → Int Source #

Typeable a ⇒ Serialise (TypeRep a)

Since: serialise-0.2.0.0

Instance details

Defined in Codec.Serialise.Class

compareByShape ∷ ∀ (rep ∷ TypeType) (t ∷ TypeType) (i ∷ Type) (j ∷ Type). Shaped t rep ⇒ t i → t j → Ordering Source #

Order two indexed types by their Shape. This is usefull for making (Singleton t) instances when we have (Shaped t r) instances, as cmpIndex can be compareByShape.