| Copyright | (c) Galois Inc 2019 |
|---|---|
| Safe Haskell | None |
| Language | Haskell2010 |
Data.Parameterized.Peano
Contents
Description
This defines a type Peano and PeanoRepr for representing a
type-level natural at runtime. These type-level numbers are defined
inductively instead of using GHC.TypeLits.
As a result, type-level computation defined recursively over these
numbers works more smoothly. (For example, see the type-level
function Repeat below.)
Note: as in NatRepr, in UNSAFE mode, the runtime representation of
these type-level natural numbers is Word64.
Synopsis
- data Peano
- type Z = Z
- type S = S
- type family Plus (a :: Peano) (b :: Peano) :: Peano where ...
- type family Minus (a :: Peano) (b :: Peano) :: Peano where ...
- type family Mul (a :: Peano) (b :: Peano) :: Peano where ...
- type family Max (a :: Peano) (b :: Peano) :: Peano where ...
- type family Min (a :: Peano) (b :: Peano) :: Peano where ...
- plusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Plus a b)
- minusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Minus a b)
- mulP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Mul a b)
- maxP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Max a b)
- minP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Min a b)
- zeroP :: PeanoRepr Z
- succP :: PeanoRepr n -> PeanoRepr (S n)
- predP :: PeanoRepr (S n) -> PeanoRepr n
- type family Repeat (m :: Peano) (f :: k -> k) (s :: k) :: k where ...
- type family CtxSizeP (ctx :: Ctx k) :: Peano where ...
- repeatP :: PeanoRepr m -> (forall a. repr a -> repr (f a)) -> repr s -> repr (Repeat m f s)
- ctxSizeP :: Assignment f ctx -> PeanoRepr (CtxSizeP ctx)
- type family Le (a :: Peano) (b :: Peano) :: Bool where ...
- type family Lt (a :: Peano) (b :: Peano) :: Bool where ...
- type family Gt (a :: Peano) (b :: Peano) :: Bool where ...
- type family Ge (a :: Peano) (b :: Peano) :: Bool where ...
- leP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Le a b)
- ltP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Lt a b)
- gtP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Gt a b)
- geP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Ge a b)
- type KnownPeano = KnownRepr PeanoRepr
- data PeanoRepr (n :: Peano)
- data PeanoView (n :: Peano) where
- peanoView :: PeanoRepr n -> PeanoView n
- viewRepr :: PeanoView n -> PeanoRepr n
- mkPeanoRepr :: Word64 -> Some PeanoRepr
- peanoValue :: PeanoRepr n -> Word64
- somePeano :: Integral a => a -> Maybe (Some PeanoRepr)
- maxPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr
- minPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr
- peanoLength :: [a] -> Some PeanoRepr
- plusCtxSizeAxiom :: forall t1 t2 f. Assignment f t1 -> Assignment f t2 -> CtxSizeP (t1 <+> t2) :~: Plus (CtxSizeP t2) (CtxSizeP t1)
- minusPlusAxiom :: forall n t t'. PeanoRepr n -> PeanoRepr t -> PeanoRepr t' -> Minus n (Plus t' t) :~: Minus (Minus n t') t
- ltMinusPlusAxiom :: forall n t t'. Lt t (Minus n t') ~ True => PeanoRepr n -> PeanoRepr t -> PeanoRepr t' -> Lt (Plus t' t) n :~: True
- class TestEquality (f :: k -> Type) where
- testEquality :: f a -> f b -> Maybe (a :~: b)
- data (a :: k) :~: (b :: k) :: forall k. k -> k -> Type where
- data Some (f :: k -> *)
Peano
Unary representation for natural numbers
Instances
| TestEquality PeanoRepr Source # | |
Defined in Data.Parameterized.Peano | |
| HashableF PeanoRepr Source # | |
| ShowF PeanoRepr Source # | |
| OrdF PeanoRepr Source # | |
Defined in Data.Parameterized.Peano | |
| DecidableEq PeanoRepr Source # | |
| IsRepr PeanoRepr Source # | |
| KnownRepr PeanoRepr Z Source # | |
| KnownRepr PeanoRepr n => KnownRepr PeanoRepr (S n :: Peano) Source # | |
Basic arithmetic
Counting
type family Repeat (m :: Peano) (f :: k -> k) (s :: k) :: k where ... Source #
Apply a constructor f n-times to an argument s
repeatP :: PeanoRepr m -> (forall a. repr a -> repr (f a)) -> repr s -> repr (Repeat m f s) Source #
Apply a constructor f n-times to an argument s
Comparisons
Runtime representation
type KnownPeano = KnownRepr PeanoRepr Source #
Implicit runtime representation
data PeanoRepr (n :: Peano) Source #
The run time value, stored as an Word64 As these are unary numbers, we don't worry about overflow.
Instances
| TestEquality PeanoRepr Source # | |
Defined in Data.Parameterized.Peano | |
| HashableF PeanoRepr Source # | |
| ShowF PeanoRepr Source # | |
| OrdF PeanoRepr Source # | |
Defined in Data.Parameterized.Peano | |
| DecidableEq PeanoRepr Source # | |
| IsRepr PeanoRepr Source # | |
| KnownRepr PeanoRepr Z Source # | |
| KnownRepr PeanoRepr n => KnownRepr PeanoRepr (S n :: Peano) Source # | |
| Eq (PeanoRepr m) Source # | |
| Show (PeanoRepr p) Source # | |
| Hashable (PeanoRepr n) Source # | |
Defined in Data.Parameterized.Peano | |
| PolyEq (PeanoRepr m) (PeanoRepr n) Source # | |
data PeanoView (n :: Peano) where Source #
When we have optimized the runtime representation, we need to have a "view" that decomposes the representation into the standard form.
'Some Peano'
peanoValue :: PeanoRepr n -> Word64 Source #
somePeano :: Integral a => a -> Maybe (Some PeanoRepr) Source #
Turn an Integral value into a PeanoRepr. Returns Nothing
if the given value is negative.
maxPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr Source #
Return the maximum of two representations.
minPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr Source #
Return the minimum of two representations.
peanoLength :: [a] -> Some PeanoRepr Source #
List length as a Peano number
Properties
plusCtxSizeAxiom :: forall t1 t2 f. Assignment f t1 -> Assignment f t2 -> CtxSizeP (t1 <+> t2) :~: Plus (CtxSizeP t2) (CtxSizeP t1) Source #
Context size commutes with context append
minusPlusAxiom :: forall n t t'. PeanoRepr n -> PeanoRepr t -> PeanoRepr t' -> Minus n (Plus t' t) :~: Minus (Minus n t') t Source #
Minus distributes over plus
ltMinusPlusAxiom :: forall n t t'. Lt t (Minus n t') ~ True => PeanoRepr n -> PeanoRepr t -> PeanoRepr t' -> Lt (Plus t' t) n :~: True Source #
We can reshuffle minus with less than
Re-exports
class TestEquality (f :: k -> Type) where #
This class contains types where you can learn the equality of two types from information contained in terms. Typically, only singleton types should inhabit this class.
Instances
data (a :: k) :~: (b :: k) :: forall k. k -> k -> Type 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
Instances
| Category ((:~:) :: k -> k -> Type) | Since: base-4.7.0.0 |
| TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
| 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 # pred :: (a :~: b) -> 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] # | |
| Eq (a :~: b) | Since: base-4.7.0.0 |
| (a ~ b, Data a) => Data (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Data Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) # toConstr :: (a :~: b) -> Constr # dataTypeOf :: (a :~: b) -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r # gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) # | |
| Ord (a :~: b) | Since: base-4.7.0.0 |
Defined in Data.Type.Equality | |
| 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 | |
| HasDict (a ~ b) (a :~: b) | |
Defined in Data.Constraint | |
data Some (f :: k -> *) Source #
Instances
| TraversableF (Some :: (k -> Type) -> Type) Source # | |
Defined in Data.Parameterized.Some | |
| FoldableF (Some :: (k -> Type) -> Type) Source # | |
Defined in Data.Parameterized.Some Methods foldMapF :: Monoid m => (forall (s :: k0). e s -> m) -> Some e -> m Source # foldrF :: (forall (s :: k0). e s -> b -> b) -> b -> Some e -> b Source # foldlF :: (forall (s :: k0). b -> e s -> b) -> b -> Some e -> b Source # foldrF' :: (forall (s :: k0). e s -> b -> b) -> b -> Some e -> b Source # foldlF' :: (forall (s :: k0). b -> e s -> b) -> b -> Some e -> b Source # toListF :: (forall (tp :: k0). f tp -> a) -> Some f -> [a] Source # | |
| FunctorF (Some :: (k -> Type) -> Type) Source # | |
| OrdC (Some :: (k -> Type) -> Type) Source # | |
| TestEqualityC (Some :: (k -> Type) -> Type) Source # | This instance demonstrates where the above class is useful: namely, in types with existential quantification. |
Defined in Data.Parameterized.ClassesC | |
| TestEquality f => Eq (Some f) Source # | |
| OrdF f => Ord (Some f) Source # | |
| ShowF f => Show (Some f) Source # | |
| HashableF f => Hashable (Some f) Source # | |
Defined in Data.Parameterized.Some | |