Safe Haskell	Safe-Inferred
Language	Haskell2010

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

class Shaped (t ∷ k → Type) (rep ∷ Type → Type) where
- shape ∷ ∀ (i ∷ k). t i → Shape rep
class Singleton (t ∷ k → Type) where
- testEql ∷ ∀ (i ∷ k) (j ∷ k). t i → t j → Maybe (i :~: j)
- cmpIndex ∷ ∀ (a ∷ k) (b ∷ k). t a → t b → Ordering
class Singleton rep ⇒ Universe (rep ∷ k → Type) (t ∷ k) where
- repOf ∷ rep t
data Any (t ∷ k → Type) where
- Any ∷ ∀ {k} (t ∷ k → Type) (i ∷ k). t i → Any t
data Some (t ∷ k → Type) where
- Some ∷ ∀ {k} (t ∷ k → Type) (i ∷ k). Singleton t ⇒ t i → Some t
data Dyn (rep ∷ Type → Type) where
- Dyn ∷ ∀ (rep ∷ Type → Type) i. Singleton rep ⇒ rep i → i → Dyn rep
data Shape (rep ∷ Type → Type) where
- Nullary ∷ ∀ (rep ∷ Type → Type). Int → Shape rep
- Nary ∷ ∀ (rep ∷ Type → Type). Int → [Shape rep] → Shape rep
- Esc ∷ ∀ (rep ∷ Type → Type) t. (Singleton rep, Ord t) ⇒ rep t → t → Shape rep
type Eql (x ∷ k) (y ∷ k) = x :~: y
data (a ∷ k) :~: (b ∷ k) where
- Refl ∷ ∀ {k} (a ∷ k). a :~: a
data TypeRep (a ∷ k)
compareByShape ∷ ∀ (rep ∷ Type → Type) t i j. Shaped t rep ⇒ t i → t j → Ordering

Documentation

class Shaped (t ∷ k → Type) (rep ∷ Type → Type) 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 ∷ ∀ (i ∷ k). t i → Shape rep Source #

class Singleton (t ∷ k → Type) 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 ∷ ∀ (i ∷ k) (j ∷ k). t i → t j → Maybe (i :~: j) Source #

cmpIndex ∷ ∀ (a ∷ k) (b ∷ k). t a → t b → Ordering Source #

Instances

Instances details

Singleton (TypeRep ∷ k → Type) Source #
Instance details Defined in Data.Universe Methods testEql ∷ ∀ (i ∷ k) (j ∷ k). TypeRep i → TypeRep j → Maybe (i :~: j) Source # cmpIndex ∷ ∀ (a ∷ k) (b ∷ k). TypeRep a → TypeRep b → Ordering Source #

class Singleton rep ⇒ Universe (rep ∷ k → Type) (t ∷ k) 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 ∷ k → Type) where Source #

Hide the index for any indexed type t

Constructors

Any ∷ ∀ {k} (t ∷ k → Type) (i ∷ k). t i → Any t

Instances

Instances details

(∀ (i ∷ k). Show (t i)) ⇒ Show (Any t) Source #
Instance details Defined in Data.Universe Methods showsPrec ∷ Int → Any t → ShowS # show ∷ Any t → String # showList ∷ [Any t] → ShowS #

data Some (t ∷ k → Type) where Source #

Hide the index for a singleton type t

Constructors

Some ∷ ∀ {k} (t ∷ k → Type) (i ∷ k). Singleton t ⇒ t i → Some t

Instances

Instances details

Eq (Some r) Source #
Instance details Defined in Data.Universe Methods (==) ∷ Some r → Some r → Bool # (/=) ∷ Some r → Some r → Bool #
Ord (Some r) Source #
Instance details Defined in Data.Universe Methods compare ∷ Some r → Some r → Ordering # (<) ∷ Some r → Some r → Bool # (<=) ∷ Some r → Some r → Bool # (>) ∷ Some r → Some r → Bool # (>=) ∷ Some r → Some r → Bool # max ∷ Some r → Some r → Some r # min ∷ Some r → Some r → Some r #

data Dyn (rep ∷ Type → Type) where Source #

Constructors

Dyn ∷ ∀ (rep ∷ Type → Type) i. Singleton rep ⇒ rep i → i → Dyn rep

data Shape (rep ∷ Type → Type) where Source #

Constructors

Nullary ∷ ∀ (rep ∷ Type → Type). Int → Shape rep
Nary ∷ ∀ (rep ∷ Type → Type). Int → [Shape rep] → Shape rep
Esc ∷ ∀ (rep ∷ Type → Type) t. (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 # (/=) ∷ Shape rep → Shape rep → Bool #
Ord (Shape rep) Source #
Instance details Defined in Data.Universe Methods compare ∷ Shape rep → Shape rep → Ordering # (<) ∷ Shape rep → Shape rep → Bool # (<=) ∷ Shape rep → Shape rep → Bool # (>) ∷ Shape rep → Shape rep → Bool # (>=) ∷ Shape rep → Shape rep → Bool # max ∷ Shape rep → Shape rep → Shape rep # min ∷ Shape rep → Shape rep → Shape rep #

type Eql (x ∷ k) (y ∷ k) = x :~: y Source #

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

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

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 GHC.Internal.Data.Type.Equality Methods testEquality ∷ ∀ (a0 ∷ k) (b ∷ k). (a :~: a0) → (a :~: b) → Maybe (a0 :~: b) #
NFData2 ((:~:) ∷ Type → Type → Type)	Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf2 ∷ (a → ()) → (b → ()) → (a :~: b) → () #
NFData1 ((:~:) a)	Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf ∷ (a0 → ()) → (a :~: a0) → () #
NFData (a :~: b)	Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods rnf ∷ (a :~: b) → () #
a ~ b ⇒ Bounded (a :~: b)	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods minBound ∷ a :~: b # maxBound ∷ a :~: b #
a ~ b ⇒ Enum (a :~: b)	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods succ ∷ (a :~: b) → a :~: b # pred ∷ (a :~: b) → a :~: b # toEnum ∷ Int → a :~: b # fromEnum ∷ (a :~: b) → Int # enumFrom ∷ (a :~: b) → [a :~: b] # enumFromThen ∷ (a :~: b) → (a :~: b) → [a :~: b] # enumFromTo ∷ (a :~: b) → (a :~: b) → [a :~: b] # enumFromThenTo ∷ (a :~: b) → (a :~: b) → (a :~: b) → [a :~: b] #
a ~ b ⇒ Read (a :~: b)	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods readsPrec ∷ Int → ReadS (a :~: b) # readList ∷ ReadS [a :~: b] # readPrec ∷ ReadPrec (a :~: b) # readListPrec ∷ ReadPrec [a :~: b] #
Show (a :~: b)	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods showsPrec ∷ Int → (a :~: b) → ShowS # show ∷ (a :~: b) → String # showList ∷ [a :~: b] → ShowS #
Eq (a :~: b)	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods (==) ∷ (a :~: b) → (a :~: b) → Bool # (/=) ∷ (a :~: b) → (a :~: b) → Bool #
Ord (a :~: b)	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods compare ∷ (a :~: b) → (a :~: b) → Ordering # (<) ∷ (a :~: b) → (a :~: b) → Bool # (<=) ∷ (a :~: b) → (a :~: b) → Bool # (>) ∷ (a :~: b) → (a :~: b) → Bool # (>=) ∷ (a :~: b) → (a :~: b) → Bool # max ∷ (a :~: b) → (a :~: b) → a :~: b # min ∷ (a :~: b) → (a :~: b) → a :~: b #

data TypeRep (a ∷ k) #

TypeRep is a concrete representation of a (monomorphic) type. TypeRep supports reasonably efficient equality. See Note [Grand plan for Typeable] in GHC.Tc.Instance.Typeable

Instances

Instances details

Singleton (TypeRep ∷ k → Type) Source #
Instance details Defined in Data.Universe Methods testEql ∷ ∀ (i ∷ k) (j ∷ k). TypeRep i → TypeRep j → Maybe (i :~: j) Source # cmpIndex ∷ ∀ (a ∷ k) (b ∷ k). TypeRep a → TypeRep b → Ordering Source #
TestEquality (TypeRep ∷ k → Type)
Instance details Defined in GHC.Internal.Data.Typeable.Internal Methods testEquality ∷ ∀ (a ∷ k) (b ∷ k). TypeRep a → TypeRep b → Maybe (a :~: b) #
NFData (TypeRep a)	Since: deepseq-1.4.8.0
Instance details Defined in Control.DeepSeq Methods rnf ∷ TypeRep a → () #
Show (TypeRep a)
Instance details Defined in GHC.Internal.Data.Typeable.Internal Methods showsPrec ∷ Int → TypeRep a → ShowS # show ∷ TypeRep a → String # showList ∷ [TypeRep a] → ShowS #
Eq (TypeRep a)	Since: base-2.1
Instance details Defined in GHC.Internal.Data.Typeable.Internal Methods (==) ∷ TypeRep a → TypeRep a → Bool # (/=) ∷ TypeRep a → TypeRep a → Bool #
Ord (TypeRep a)	Since: base-4.4.0.0
Instance details Defined in GHC.Internal.Data.Typeable.Internal Methods compare ∷ TypeRep a → TypeRep a → Ordering # (<) ∷ TypeRep a → TypeRep a → Bool # (<=) ∷ TypeRep a → TypeRep a → Bool # (>) ∷ TypeRep a → TypeRep a → Bool # (>=) ∷ TypeRep a → TypeRep a → Bool # max ∷ TypeRep a → TypeRep a → TypeRep a # min ∷ TypeRep a → TypeRep a → TypeRep a #
Hashable (TypeRep a)
Instance details Defined in Data.Hashable.Class Methods hashWithSalt ∷ Int → TypeRep a → Int Source # hash ∷ TypeRep a → Int Source #

compareByShape ∷ ∀ (rep ∷ Type → Type) t i j. 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.