Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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
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 # | |
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 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 |