| Safe Haskell | Safe-Inferred |
|---|---|
| Language | GHC2021 |
Plutarch.Enum
Contents
Synopsis
- class POrd a => PCountable (a :: S -> Type) where
- psuccessor :: forall (s :: S). Term s (a :--> a)
- psuccessorN :: forall (s :: S). Term s (PPositive :--> (a :--> a))
- class PCountable a => PEnumerable (a :: S -> Type) where
- ppredecessor :: forall (s :: S). Term s (a :--> a)
- ppredecessorN :: forall (s :: S). Term s (PPositive :--> (a :--> a))
Type classes
class POrd a => PCountable (a :: S -> Type) where Source #
A notion of 'next' value. More formally, instances of this type class are discrete linear orders with no maximal element.
Laws
x /= psuccessor x
y < x=psuccessor y <= xx < psuccessor y=x <= y
If you define psuccessorN, you must also ensure the following hold; the
default implementation ensures this.
psuccessorN 1=psuccessorpsuccessorN n . psuccessorN m=psuccessorN (n + m)
Law 1 ensures no value is its own successor. Laws 2 and 3 ensure that there
are no 'gaps': every value is 'reachable' from any lower value by a
finite number of applications of successor.
Since: 1.10.0
Minimal complete definition
Methods
psuccessor :: forall (s :: S). Term s (a :--> a) Source #
Since: 1.10.0
psuccessorN :: forall (s :: S). Term s (PPositive :--> (a :--> a)) Source #
The default implementation of this function is inefficient: if at all possible, give instances an optimized version that doesn't require recursion.
Since: 1.10.0
Instances
| PCountable PInteger Source # | Since: 1.10.0 |
| PCountable PPositive Source # | Since: 1.10.0 |
class PCountable a => PEnumerable (a :: S -> Type) where Source #
Similar to PCountable, but has the ability to get a 'previous' value as
well. More formally, instances of this type class are discrete linear orders
with no maximal or minimal element.
Laws
ppredecessor . psuccessor=psuccessor . ppredecessor=id
If you define ppredecessorN, you must also ensure the following hold; the
default implementation ensures this.
ppredecessorN 1=ppredecessorppredecessorN n . ppredecessorN m=ppredecessorN (n + m)
From Law 1, we obtain the following theorem:
x /= predecessor x
Since: 1.10.0
Minimal complete definition
Methods
ppredecessor :: forall (s :: S). Term s (a :--> a) Source #
Since: 1.10.0
ppredecessorN :: forall (s :: S). Term s (PPositive :--> (a :--> a)) Source #
The default implementation of this function is inefficient: if at all possible, give instances an optimized version that doesn't require recursion.
Since: 1.10.0