| Copyright | (c) Galois Inc 2019 |
|---|---|
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Data.Parameterized.Peano
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 :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
- data (a :: k) :~: (b :: k) where
- data Some (f :: k -> Type)
Peano
Unary representation for natural numbers
Instances
| TestEquality PeanoRepr Source # | |
Defined in Data.Parameterized.Peano | |
| HashableF PeanoRepr Source # | |
| OrdF PeanoRepr Source # | |
Defined in Data.Parameterized.Peano Methods compareF :: forall (x :: k) (y :: k). PeanoRepr x -> PeanoRepr y -> OrderingF x y Source # leqF :: forall (x :: k) (y :: k). PeanoRepr x -> PeanoRepr y -> Bool Source # ltF :: forall (x :: k) (y :: k). PeanoRepr x -> PeanoRepr y -> Bool Source # geqF :: forall (x :: k) (y :: k). PeanoRepr x -> PeanoRepr y -> Bool Source # gtF :: forall (x :: k) (y :: k). PeanoRepr x -> PeanoRepr y -> Bool Source # | |
| ShowF PeanoRepr Source # | |
| 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 # | |
| OrdF PeanoRepr Source # | |
Defined in Data.Parameterized.Peano Methods compareF :: forall (x :: k) (y :: k). PeanoRepr x -> PeanoRepr y -> OrderingF x y Source # leqF :: forall (x :: k) (y :: k). PeanoRepr x -> PeanoRepr y -> Bool Source # ltF :: forall (x :: k) (y :: k). PeanoRepr x -> PeanoRepr y -> Bool Source # geqF :: forall (x :: k) (y :: k). PeanoRepr x -> PeanoRepr y -> Bool Source # gtF :: forall (x :: k) (y :: k). PeanoRepr x -> PeanoRepr y -> Bool Source # | |
| ShowF PeanoRepr Source # | |
| DecidableEq PeanoRepr Source # | |
| IsRepr PeanoRepr Source # | |
| KnownRepr PeanoRepr Z Source # | |
| KnownRepr PeanoRepr n => KnownRepr PeanoRepr (S n :: Peano) Source # | |
| Show (PeanoRepr p) Source # | |
| Eq (PeanoRepr m) 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.
The result should be Just Refl if and only if the types applied to f are
equal:
testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b
Typically, only singleton types should inhabit this class. In that case type argument equality coincides with term equality:
testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b ⟺ x = y
isJust (testEquality x y) = x == y
Singleton types are not required, however, and so the latter two would-be laws are not in fact valid in general.
Methods
testEquality :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b) #
Conditionally prove the equality of a and b.
Instances
data (a :: k) :~: (b :: k) 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, 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 :: forall r r'. (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) # | |
| 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] # | |
| 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 | |
| HasDict (a ~ b) (a :~: b) | |
data Some (f :: k -> Type) Source #
Instances
| 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 | |
| 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 # | |
| TraversableF (Some :: (k -> Type) -> Type) Source # | |
Defined in Data.Parameterized.Some | |
| ShowF f => Show (Some f) Source # | |
| TestEquality f => Eq (Some f) Source # | |
| OrdF f => Ord (Some f) Source # | |
| (HashableF f, TestEquality f) => Hashable (Some f) Source # | |
Defined in Data.Parameterized.Some | |