Copyright | (c) Galois Inc 2019 |
---|---|
Safe Haskell | None |
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 :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Plus a b)
- minusP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Minus a b)
- mulP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Mul a b)
- maxP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Max a b)
- minP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Min a b)
- zeroP :: PeanoRepr Z
- succP :: forall (n :: Peano). PeanoRepr n -> PeanoRepr (S n)
- predP :: forall (n :: Peano). 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 :: forall {k} (m :: Peano) repr (f :: k -> k) (s :: k). PeanoRepr m -> (forall (a :: k). repr a -> repr (f a)) -> repr s -> repr (Repeat m f s)
- ctxSizeP :: forall {k} (f :: k -> Type) (ctx :: Ctx k). 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 :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> BoolRepr (Le a b)
- ltP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> BoolRepr (Lt a b)
- gtP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> BoolRepr (Gt a b)
- geP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> BoolRepr (Ge a b)
- type KnownPeano = KnownRepr PeanoRepr
- data PeanoRepr (n :: Peano)
- data PeanoView (n :: Peano) where
- peanoView :: forall (n :: Peano). PeanoRepr n -> PeanoView n
- viewRepr :: forall (n :: Peano). PeanoView n -> PeanoRepr n
- mkPeanoRepr :: Word64 -> Some PeanoRepr
- peanoValue :: PeanoRepr n -> Word64
- somePeano :: Integral a => a -> Maybe (Some PeanoRepr)
- maxPeano :: forall (m :: Peano) (n :: Peano). PeanoRepr m -> PeanoRepr n -> Some PeanoRepr
- minPeano :: forall (m :: Peano) (n :: Peano). PeanoRepr m -> PeanoRepr n -> Some PeanoRepr
- peanoLength :: [a] -> Some PeanoRepr
- plusCtxSizeAxiom :: forall {k} (t1 :: Ctx k) (t2 :: Ctx k) (f :: k -> Type). Assignment f t1 -> Assignment f t2 -> CtxSizeP (t1 <+> t2) :~: Plus (CtxSizeP t2) (CtxSizeP t1)
- minusPlusAxiom :: forall (n :: Peano) (t :: Peano) (t' :: Peano). PeanoRepr n -> PeanoRepr t -> PeanoRepr t' -> Minus n (Plus t' t) :~: Minus (Minus n t') t
- ltMinusPlusAxiom :: forall (n :: Peano) (t :: Peano) (t' :: Peano). 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 | |
EqF PeanoRepr Source # | |
HashableF PeanoRepr Source # | |
OrdF PeanoRepr Source # | |
Defined in Data.Parameterized.Peano Methods compareF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> OrderingF x y Source # leqF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> Bool Source # ltF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> Bool Source # geqF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> Bool Source # gtF :: forall (x :: Peano) (y :: Peano). 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
plusP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Plus a b) Source #
Addition
minusP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Minus a b) Source #
Subtraction
mulP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Mul a b) Source #
Multiplication
maxP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Max a b) Source #
Maximum
minP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> PeanoRepr (Min a b) Source #
Minimum
predP :: forall (n :: Peano). PeanoRepr (S n) -> PeanoRepr n Source #
Get the predecessor (decrement)
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 :: forall {k} (m :: Peano) repr (f :: k -> k) (s :: k). PeanoRepr m -> (forall (a :: k). repr a -> repr (f a)) -> repr s -> repr (Repeat m f s) Source #
Apply a constructor f
n-times to an argument s
ctxSizeP :: forall {k} (f :: k -> Type) (ctx :: Ctx k). Assignment f ctx -> PeanoRepr (CtxSizeP ctx) Source #
Calculate the size of a context
Comparisons
leP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> BoolRepr (Le a b) Source #
Less-than-or-equal-to
ltP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> BoolRepr (Lt a b) Source #
Less-than
gtP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> BoolRepr (Gt a b) Source #
Greater-than
geP :: forall (a :: Peano) (b :: Peano). PeanoRepr a -> PeanoRepr b -> BoolRepr (Ge a b) Source #
Greater-than-or-equal-to
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 | |
EqF PeanoRepr Source # | |
HashableF PeanoRepr Source # | |
OrdF PeanoRepr Source # | |
Defined in Data.Parameterized.Peano Methods compareF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> OrderingF x y Source # leqF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> Bool Source # ltF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> Bool Source # geqF :: forall (x :: Peano) (y :: Peano). PeanoRepr x -> PeanoRepr y -> Bool Source # gtF :: forall (x :: Peano) (y :: Peano). 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.
peanoView :: forall (n :: Peano). PeanoRepr n -> PeanoView n Source #
Test whether a number is Zero or Successor
viewRepr :: forall (n :: Peano). PeanoView n -> PeanoRepr n Source #
convert the view back to the runtime representation
'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 :: forall (m :: Peano) (n :: Peano). PeanoRepr m -> PeanoRepr n -> Some PeanoRepr Source #
Return the maximum of two representations.
minPeano :: forall (m :: Peano) (n :: Peano). 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 {k} (t1 :: Ctx k) (t2 :: Ctx k) (f :: k -> Type). Assignment f t1 -> Assignment f t2 -> CtxSizeP (t1 <+> t2) :~: Plus (CtxSizeP t2) (CtxSizeP t1) Source #
Context size commutes with context append
minusPlusAxiom :: forall (n :: Peano) (t :: Peano) (t' :: Peano). PeanoRepr n -> PeanoRepr t -> PeanoRepr t' -> Minus n (Plus t' t) :~: Minus (Minus n t') t Source #
Minus distributes over plus
ltMinusPlusAxiom :: forall (n :: Peano) (t :: Peano) (t' :: Peano). 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 #
Methods
testEquality :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b) #
Instances
TestEquality SNat | |
Defined in GHC.TypeNats Methods testEquality :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) # | |
TestEquality NatRepr Source # | |
Defined in Data.Parameterized.NatRepr.Internal Methods testEquality :: forall (a :: Nat) (b :: Nat). NatRepr a -> NatRepr b -> Maybe (a :~: b) # | |
TestEquality PeanoRepr Source # | |
Defined in Data.Parameterized.Peano | |
TestEquality BoolRepr Source # | |
Defined in Data.Parameterized.BoolRepr Methods testEquality :: forall (a :: Bool) (b :: Bool). BoolRepr a -> BoolRepr b -> Maybe (a :~: b) # | |
TestEquality SChar | |
Defined in GHC.TypeLits Methods testEquality :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> Maybe (a :~: b) # | |
TestEquality SSymbol | |
Defined in GHC.TypeLits Methods testEquality :: forall (a :: Symbol) (b :: Symbol). SSymbol a -> SSymbol b -> Maybe (a :~: b) # | |
TestEquality SymbolRepr Source # | |
Defined in Data.Parameterized.SymbolRepr Methods testEquality :: forall (a :: Symbol) (b :: Symbol). SymbolRepr a -> SymbolRepr b -> Maybe (a :~: b) # | |
TestEquality (TypeRep :: k -> Type) | |
Defined in Data.Typeable.Internal Methods testEquality :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b) # | |
TestEquality (Nonce :: k -> Type) Source # | |
Defined in Data.Parameterized.Nonce.Unsafe Methods testEquality :: forall (a :: k) (b :: k). Nonce a -> Nonce b -> Maybe (a :~: b) # | |
TestEquality ((:~:) a :: k -> Type) | |
Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) # | |
TestEquality (Index ctx :: k -> Type) Source # | |
Defined in Data.Parameterized.Context.Unsafe Methods testEquality :: forall (a :: k) (b :: k). Index ctx a -> Index ctx b -> Maybe (a :~: b) # | |
TestEquality (Index l :: k -> Type) Source # | |
Defined in Data.Parameterized.List Methods testEquality :: forall (a :: k) (b :: k). Index l a -> Index l b -> Maybe (a :~: b) # | |
TestEquality (Nonce s :: k -> Type) Source # | |
Defined in Data.Parameterized.Nonce Methods testEquality :: forall (a :: k) (b :: k). Nonce s a -> Nonce s b -> Maybe (a :~: b) # | |
TestEquality ((:~~:) a :: k -> Type) | |
Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) # | |
TestEquality f => TestEquality (Compose f g :: k2 -> Type) | |
Defined in Data.Functor.Compose Methods testEquality :: forall (a :: k2) (b :: k2). Compose f g a -> Compose f g b -> Maybe (a :~: b) # | |
TestEquality f => TestEquality (Assignment f :: Ctx k -> Type) Source # | |
Defined in Data.Parameterized.Context.Unsafe Methods testEquality :: forall (a :: Ctx k) (b :: Ctx k). Assignment f a -> Assignment f b -> Maybe (a :~: b) # | |
TestEquality f => TestEquality (List f :: [k] -> Type) Source # | |
Defined in Data.Parameterized.List Methods testEquality :: forall (a :: [k]) (b :: [k]). List f a -> List f b -> Maybe (a :~: b) # | |
(TestEquality f, TestEquality g) => TestEquality (PairRepr f g :: (k1, k2) -> Type) Source # | |
Defined in Data.Parameterized.DataKind Methods testEquality :: forall (a :: (k1, k2)) (b :: (k1, k2)). PairRepr f g a -> PairRepr f g b -> Maybe (a :~: b) # |
data (a :: k) :~: (b :: k) where #
Instances
Category ((:~:) :: k -> k -> Type) | |
TestCoercion ((:~:) a :: k -> Type) | |
Defined in Data.Type.Coercion Methods testCoercion :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) | |
TestEquality ((:~:) a :: k -> Type) | |
Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) # | |
NFData2 ((:~:) :: Type -> Type -> Type) | |
Defined in Control.DeepSeq | |
NFData1 ((:~:) a) | |
Defined in Control.DeepSeq | |
(a ~ b, Data a) => Data (a :~: b) | |
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) | |
Defined in Data.Type.Equality | |
a ~ b => Enum (a :~: b) | |
Defined in Data.Type.Equality | |
a ~ b => Read (a :~: b) | |
Defined in Data.Type.Equality | |
Show (a :~: b) | |
NFData (a :~: b) | |
Defined in Control.DeepSeq | |
Eq (a :~: b) | |
Ord (a :~: b) | |
Defined in Data.Type.Equality | |
HasDict (a ~ b) (a :~: b) | |
Defined in Data.Constraint |
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 :: k). e s -> m) -> Some e -> m Source # foldrF :: (forall (s :: k). e s -> b -> b) -> b -> Some e -> b Source # foldlF :: (forall (s :: k). b -> e s -> b) -> b -> Some e -> b Source # foldrF' :: (forall (s :: k). e s -> b -> b) -> b -> Some e -> b Source # foldlF' :: (forall (s :: k). b -> e s -> b) -> b -> Some e -> b Source # toListF :: (forall (tp :: k). f tp -> a) -> Some f -> [a] Source # | |
FunctorF (Some :: (k -> Type) -> Type) Source # | |
TraversableF (Some :: (k -> Type) -> Type) Source # | |
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 |