| 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
Hide the index for a singleton type t
Constructors
| Nullary ∷ Int → Shape rep | |
| Nary ∷ Int → [Shape rep] → Shape rep | |
| Esc ∷ (Singleton rep, Ord t) ⇒ rep t → t → Shape rep |
Instances
| Eq (Shape rep) Source # | |
| Ord (Shape rep) Source # | |
Defined in Data.Universe | |
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
Instances
| TestEquality ((:~:) a ∷ k → Type) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
| 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) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
| NFData1 ((:~:) a) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
| a ~ b ⇒ Bounded (a :~: b) | Since: base-4.7.0.0 |
| a ~ b ⇒ Enum (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality Methods succ ∷ (a :~: b) → a :~: b Source # pred ∷ (a :~: b) → a :~: b Source # toEnum ∷ Int → 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 |
| Show (a :~: b) | Since: base-4.7.0.0 |
| NFData (a :~: b) | Since: deepseq-1.4.3.0 |
Defined in Control.DeepSeq | |
| Eq (a :~: b) | Since: base-4.7.0.0 |
| Ord (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
A concrete representation of a (monomorphic) type.
TypeRep supports reasonably efficient equality.
Instances
| TestEquality (TypeRep ∷ k → Type) | |
Defined in Data.Typeable.Internal | |
| 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) | Since: base-2.1 |
| Ord (TypeRep a) | Since: base-4.4.0.0 |
Defined in Data.Typeable.Internal | |
| Hashable (TypeRep a) | |
| Typeable a ⇒ Serialise (TypeRep a) | Since: serialise-0.2.0.0 |