| 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 rep where
- class Singleton t where
- class Singleton rep ⇒ Universe rep t where
- repOf ∷ rep t
- data Any t where
- data Some t where
- data Dyn rep where
- data Shape rep where
- type Eql x y = x :~: y
- data (a ∷ k) :~: (b ∷ k) where
- data TypeRep (a ∷ k)
- compareByShape ∷ ∀ (rep ∷ Type → Type) (t ∷ Type → Type) (i ∷ Type) (j ∷ Type). Shaped t rep ⇒ t i → t j → Ordering
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.
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
Hide the index for any indexed type t
Constructors
| Nullary ∷ Int → Shape rep | |
| Nary ∷ Int → [Shape rep] → Shape rep | |
| Esc ∷ (Singleton rep, Ord t) ⇒ rep t → t → Shape rep |
data (a ∷ k) :~: (b ∷ k) where #
Instances
| TestEquality ((:~:) a ∷ k → Type) | |
Defined in Data.Type.Equality Methods testEquality ∷ ∀ (a0 ∷ k0) (b ∷ k0). (a :~: a0) → (a :~: b) → Maybe (a0 :~: b) | |
| GCompare ((:~:) a ∷ k → Type) | |
| GEq ((:~:) a ∷ k → Type) | |
| GRead ((:~:) a ∷ k → Type) | |
Defined in Data.GADT.Internal | |
| GShow ((:~:) a ∷ k → Type) | |
Defined in Data.GADT.Internal | |
| NFData2 ((:~:) ∷ Type → Type → Type) | |
Defined in Control.DeepSeq | |
| NFData1 ((:~:) a) | |
Defined in Control.DeepSeq | |
| a ~ b ⇒ Bounded (a :~: b) | |
| a ~ b ⇒ Enum (a :~: b) | |
| a ~ b ⇒ Read (a :~: b) | |
| Show (a :~: b) | |
| NFData (a :~: b) | |
Defined in Control.DeepSeq | |
| Eq (a :~: b) | |
| Ord (a :~: b) | |
Defined in Data.Type.Equality | |
Instances
| TestEquality (TypeRep ∷ k → Type) | |
Defined in Data.Typeable.Internal Methods testEquality ∷ ∀ (a ∷ k0) (b ∷ k0). TypeRep a → TypeRep b → Maybe (a :~: b) | |
| Singleton (TypeRep ∷ k → Type) Source # | |
| GCompare (TypeRep ∷ k → Type) | |
| GEq (TypeRep ∷ k → Type) | |
| GShow (TypeRep ∷ k → Type) | |
Defined in Data.GADT.Internal | |
| Show (TypeRep a) | |
| Eq (TypeRep a) | |
| Ord (TypeRep a) | |
Defined in Data.Typeable.Internal | |
| Hashable (TypeRep a) | |
| Typeable a ⇒ Serialise (TypeRep a) | Since: serialise-0.2.0.0 |
compareByShape ∷ ∀ (rep ∷ Type → Type) (t ∷ Type → Type) (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.