Data.Parameterized.Peano

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.

Peano

data Peano

Unary representation for natural numbers

Instances

TestEquality PeanoRepr

Defined in Data.Parameterized.Peano

Methods

testEquality :: PeanoRepr a -> PeanoRepr b -> Maybe (a :~: b)

HashableF PeanoRepr

Defined in Data.Parameterized.Peano

Methods

hashWithSaltF :: Int -> PeanoRepr tp -> Int

hashF :: PeanoRepr tp -> Int

ShowF PeanoRepr

Defined in Data.Parameterized.Peano

Methods

withShow :: p PeanoRepr -> q tp -> (Show (PeanoRepr tp) -> a) -> a

showF :: PeanoRepr tp -> String

showsPrecF :: Int -> PeanoRepr tp -> String -> String

OrdF PeanoRepr

Defined in Data.Parameterized.Peano

Methods

compareF :: PeanoRepr x -> PeanoRepr y -> OrderingF x y

leqF :: PeanoRepr x -> PeanoRepr y -> Bool

ltF :: PeanoRepr x -> PeanoRepr y -> Bool

geqF :: PeanoRepr x -> PeanoRepr y -> Bool

gtF :: PeanoRepr x -> PeanoRepr y -> Bool

DecidableEq PeanoRepr

Defined in Data.Parameterized.Peano

Methods

decEq :: PeanoRepr a -> PeanoRepr b -> Either (a :~: b) ((a :~: b) -> Void)

IsRepr PeanoRepr

Defined in Data.Parameterized.WithRepr

Methods

withRepr :: PeanoRepr a -> (KnownRepr PeanoRepr a -> r) -> r

KnownRepr PeanoRepr Z

Defined in Data.Parameterized.Peano

Methods

knownRepr :: PeanoRepr Z

KnownRepr PeanoRepr n => KnownRepr PeanoRepr (S n :: Peano)

Defined in Data.Parameterized.Peano

Methods

knownRepr :: PeanoRepr (S n)

type Z = Z

Peano zero

type S = S

Peano successor

Basic arithmetic

type family Plus (a :: Peano) (b :: Peano) :: Peano where ...

Addition

Equations

Plus Z b = b

Plus (S a) b = S (Plus a b)

type family Minus (a :: Peano) (b :: Peano) :: Peano where ...

Subtraction

Equations

Minus Z b = Z

Minus (S a) (S b) = Minus a b

Minus a Z = a

type family Mul (a :: Peano) (b :: Peano) :: Peano where ...

Multiplication

Equations

Mul Z b = Z

Mul (S a) b = Plus a (Mul a b)

type family Max (a :: Peano) (b :: Peano) :: Peano where ...

Maximum

Equations

Max Z b = b

Max a Z = a

Max (S a) (S b) = S (Max a b)

type family Min (a :: Peano) (b :: Peano) :: Peano where ...

Minimum

Equations

Min Z b = Z

Min a Z = Z

Min (S a) (S b) = S (Min a b)

plusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Plus a b)

Addition

minusP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Minus a b)

Subtraction

mulP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Mul a b)

Multiplication

maxP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Max a b)

Maximum

minP :: PeanoRepr a -> PeanoRepr b -> PeanoRepr (Min a b)

Minimum

zeroP :: PeanoRepr Z

Zero

succP :: PeanoRepr n -> PeanoRepr (S n)

Successor, Increment

predP :: PeanoRepr (S n) -> PeanoRepr n

Get the predecessor (decrement)

Counting

type family Repeat (m :: Peano) (f :: k -> k) (s :: k) :: k where ...

Apply a constructor f n-times to an argument s

Equations

Repeat Z f s = s

Repeat (S m) f s = f (Repeat m f s)

type family CtxSizeP (ctx :: Ctx k) :: Peano where ...

Calculate the size of a context

Equations

CtxSizeP EmptyCtx = Z

CtxSizeP (xs ::> x) = S (CtxSizeP xs)

repeatP :: PeanoRepr m -> (forall a. repr a -> repr (f a)) -> repr s -> repr (Repeat m f s)

Apply a constructor f n-times to an argument s

ctxSizeP :: Assignment f ctx -> PeanoRepr (CtxSizeP ctx)

Calculate the size of a context

Comparisons

type family Le (a :: Peano) (b :: Peano) :: Bool where ...

Less-than-or-equal

Equations

Le Z b = True

Le a Z = False

Le (S a) (S b) = Le a b

type family Lt (a :: Peano) (b :: Peano) :: Bool where ...

Less-than

Equations

Lt a b = Le (S a) b

type family Gt (a :: Peano) (b :: Peano) :: Bool where ...

Greater-than

Equations

Gt a b = Le b a

type family Ge (a :: Peano) (b :: Peano) :: Bool where ...

Greater-than-or-equal

Equations

Ge a b = Lt b a

leP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Le a b)

Less-than-or-equal-to

ltP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Lt a b)

Less-than

gtP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Gt a b)

Greater-than

geP :: PeanoRepr a -> PeanoRepr b -> BoolRepr (Ge a b)

Greater-than-or-equal-to

Runtime representation

type KnownPeano = KnownRepr PeanoRepr

Implicit runtime representation

data PeanoRepr (n :: Peano)

The run time value, stored as an Word64 As these are unary numbers, we don't worry about overflow.

Instances

TestEquality PeanoRepr

Defined in Data.Parameterized.Peano

Methods

testEquality :: PeanoRepr a -> PeanoRepr b -> Maybe (a :~: b)

HashableF PeanoRepr

Defined in Data.Parameterized.Peano

Methods

hashWithSaltF :: Int -> PeanoRepr tp -> Int

hashF :: PeanoRepr tp -> Int

ShowF PeanoRepr

Defined in Data.Parameterized.Peano

Methods

withShow :: p PeanoRepr -> q tp -> (Show (PeanoRepr tp) -> a) -> a

showF :: PeanoRepr tp -> String

showsPrecF :: Int -> PeanoRepr tp -> String -> String

OrdF PeanoRepr

Defined in Data.Parameterized.Peano

Methods

compareF :: PeanoRepr x -> PeanoRepr y -> OrderingF x y

leqF :: PeanoRepr x -> PeanoRepr y -> Bool

ltF :: PeanoRepr x -> PeanoRepr y -> Bool

geqF :: PeanoRepr x -> PeanoRepr y -> Bool

gtF :: PeanoRepr x -> PeanoRepr y -> Bool

DecidableEq PeanoRepr

Defined in Data.Parameterized.Peano

Methods

decEq :: PeanoRepr a -> PeanoRepr b -> Either (a :~: b) ((a :~: b) -> Void)

IsRepr PeanoRepr

Defined in Data.Parameterized.WithRepr

Methods

withRepr :: PeanoRepr a -> (KnownRepr PeanoRepr a -> r) -> r

KnownRepr PeanoRepr Z

Defined in Data.Parameterized.Peano

Methods

knownRepr :: PeanoRepr Z

KnownRepr PeanoRepr n => KnownRepr PeanoRepr (S n :: Peano)

Defined in Data.Parameterized.Peano

Methods

knownRepr :: PeanoRepr (S n)

Eq (PeanoRepr m)

Defined in Data.Parameterized.Peano

Methods

(==) :: PeanoRepr m -> PeanoRepr m -> Bool

(/=) :: PeanoRepr m -> PeanoRepr m -> Bool

Show (PeanoRepr p)

Defined in Data.Parameterized.Peano

Methods

showsPrec :: Int -> PeanoRepr p -> ShowS

show :: PeanoRepr p -> String

showList :: [PeanoRepr p] -> ShowS

Hashable (PeanoRepr n)

Defined in Data.Parameterized.Peano

Methods

hashWithSalt :: Int -> PeanoRepr n -> Int

hash :: PeanoRepr n -> Int

PolyEq (PeanoRepr m) (PeanoRepr n)

Defined in Data.Parameterized.Peano

Methods

polyEqF :: PeanoRepr m -> PeanoRepr n -> Maybe (PeanoRepr m :~: PeanoRepr n)

polyEq :: PeanoRepr m -> PeanoRepr n -> Bool

data PeanoView (n :: Peano) where

When we have optimized the runtime representation, we need to have a "view" that decomposes the representation into the standard form.

Constructors

ZRepr :: PeanoView Z

SRepr :: PeanoRepr n -> PeanoView (S n)

peanoView :: PeanoRepr n -> PeanoView n

Test whether a number is Zero or Successor

viewRepr :: PeanoView n -> PeanoRepr n

convert the view back to the runtime representation

'Some Peano'

mkPeanoRepr :: Word64 -> Some PeanoRepr

Convert a Word64 to a PeanoRepr

peanoValue :: PeanoRepr n -> Word64

somePeano :: Integral a => a -> Maybe (Some PeanoRepr)

Turn an Integral value into a PeanoRepr. Returns Nothing if the given value is negative.

maxPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr

Return the maximum of two representations.

minPeano :: PeanoRepr m -> PeanoRepr n -> Some PeanoRepr

Return the minimum of two representations.

peanoLength :: [a] -> Some PeanoRepr

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)

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

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

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.

Methods

testEquality :: f a -> f b -> Maybe (a :~: b)

Conditionally prove the equality of a and b.

Instances

TestEquality BoolRepr

Defined in Data.Parameterized.BoolRepr

Methods

testEquality :: BoolRepr a -> BoolRepr b -> Maybe (a :~: b)

TestEquality NatRepr

Defined in Data.Parameterized.NatRepr.Internal

Methods

testEquality :: NatRepr a -> NatRepr b -> Maybe (a :~: b)

TestEquality SymbolRepr

Defined in Data.Parameterized.SymbolRepr

Methods

testEquality :: SymbolRepr a -> SymbolRepr b -> Maybe (a :~: b)

TestEquality PeanoRepr

Defined in Data.Parameterized.Peano

Methods

testEquality :: PeanoRepr a -> PeanoRepr b -> Maybe (a :~: b)

TestEquality (Nonce :: k -> Type)

Defined in Data.Parameterized.Nonce.Unsafe

Methods

testEquality :: Nonce a -> Nonce b -> Maybe (a :~: b)

TestEquality (TypeRep :: k -> Type)

Defined in Data.Typeable.Internal

Methods

testEquality :: TypeRep a -> TypeRep b -> Maybe (a :~: b)

TestEquality (Nonce s :: k -> Type)

Defined in Data.Parameterized.Nonce

Methods

testEquality :: Nonce s a -> Nonce s b -> Maybe (a :~: b)

TestEquality ((:~:) a :: k -> Type)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

testEquality :: (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b)

TestEquality (Index l :: k -> Type)

Defined in Data.Parameterized.List

Methods

testEquality :: Index l a -> Index l b -> Maybe (a :~: b)

TestEquality (Index ctx :: k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

testEquality :: Index ctx a -> Index ctx b -> Maybe (a :~: b)

TestEquality ((:~~:) a :: k -> Type)

Since: base-4.10.0.0

Defined in Data.Type.Equality

Methods

testEquality :: (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b)

TestEquality f => TestEquality (Compose f g :: k1 -> Type)

Defined in Data.Parameterized.Compose

Methods

testEquality :: Compose f g a -> Compose f g b -> Maybe (a :~: b)

TestEquality f => TestEquality (List f :: [k] -> Type)

Defined in Data.Parameterized.List

Methods

testEquality :: List f a -> List f b -> Maybe (a :~: b)

TestEquality f => TestEquality (Assignment f :: Ctx k -> Type)

Defined in Data.Parameterized.Context.Unsafe

Methods

testEquality :: Assignment f a -> Assignment f b -> Maybe (a :~: b)

(TestEquality f, TestEquality g) => TestEquality (PairRepr f g :: (k1, k2) -> Type)

Defined in Data.Parameterized.DataKind

Methods

testEquality :: PairRepr f g a -> PairRepr f g b -> Maybe (a :~: b)

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

Constructors

Refl :: forall k (a :: k) (b :: k). a :~: a

Instances

Category ((:~:) :: k -> k -> Type)

Since: base-4.7.0.0

Defined in Control.Category

Methods

id :: a :~: a

(.) :: (b :~: c) -> (a :~: b) -> a :~: c

TestEquality ((:~:) a :: k -> Type)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

testEquality :: (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b)

NFData2 ((:~:) :: Type -> Type -> Type)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~: b) -> ()

NFData1 ((:~:) a)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

liftRnf :: (a0 -> ()) -> (a :~: a0) -> ()

a ~ b => Bounded (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

minBound :: a :~: b

maxBound :: a :~: b

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

toEnum :: Int -> 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

Defined in Data.Type.Equality

Methods

(==) :: (a :~: b) -> (a :~: b) -> Bool

(/=) :: (a :~: b) -> (a :~: b) -> Bool

(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

Methods

compare :: (a :~: b) -> (a :~: b) -> Ordering

(<) :: (a :~: b) -> (a :~: b) -> Bool

(<=) :: (a :~: b) -> (a :~: b) -> Bool

(>) :: (a :~: b) -> (a :~: b) -> Bool

(>=) :: (a :~: b) -> (a :~: b) -> Bool

max :: (a :~: b) -> (a :~: b) -> a :~: b

min :: (a :~: b) -> (a :~: b) -> a :~: b

a ~ b => Read (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

readsPrec :: Int -> ReadS (a :~: b)

readList :: ReadS [a :~: b]

readPrec :: ReadPrec (a :~: b)

readListPrec :: ReadPrec [a :~: b]

Show (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

showsPrec :: Int -> (a :~: b) -> ShowS

show :: (a :~: b) -> String

showList :: [a :~: b] -> ShowS

NFData (a :~: b)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

rnf :: (a :~: b) -> ()

HasDict (a ~ b) (a :~: b)

Defined in Data.Constraint

Methods

evidence :: (a :~: b) -> Dict (a ~ b)

data Some (f :: k -> *)

Instances

TraversableF (Some :: (k -> Type) -> Type)

Defined in Data.Parameterized.Some

Methods

traverseF :: Applicative m => (forall (s :: k0). e s -> m (f s)) -> Some e -> m (Some f)

FoldableF (Some :: (k -> Type) -> Type)

Defined in Data.Parameterized.Some

Methods

foldMapF :: Monoid m => (forall (s :: k0). e s -> m) -> Some e -> m

foldrF :: (forall (s :: k0). e s -> b -> b) -> b -> Some e -> b

foldlF :: (forall (s :: k0). b -> e s -> b) -> b -> Some e -> b

foldrF' :: (forall (s :: k0). e s -> b -> b) -> b -> Some e -> b

foldlF' :: (forall (s :: k0). b -> e s -> b) -> b -> Some e -> b

toListF :: (forall (tp :: k0). f tp -> a) -> Some f -> [a]

FunctorF (Some :: (k -> Type) -> Type)

Defined in Data.Parameterized.Some

Methods

fmapF :: (forall (x :: k0). f x -> g x) -> Some f -> Some g

OrdC (Some :: (k -> Type) -> Type)

Defined in Data.Parameterized.ClassesC

Methods

compareC :: (forall (x :: k0) (y :: k0). f x -> g y -> OrderingF x y) -> Some f -> Some g -> Ordering

TestEqualityC (Some :: (k -> Type) -> Type)

This instance demonstrates where the above class is useful: namely, in types with existential quantification.

Defined in Data.Parameterized.ClassesC

Methods

testEqualityC :: (forall (x :: k0) (y :: k0). f x -> f y -> Maybe (x :~: y)) -> Some f -> Some f -> Bool

TestEquality f => Eq (Some f)

Defined in Data.Parameterized.Some

Methods

(==) :: Some f -> Some f -> Bool

(/=) :: Some f -> Some f -> Bool

OrdF f => Ord (Some f)

Defined in Data.Parameterized.Some

Methods

compare :: Some f -> Some f -> Ordering

(<) :: Some f -> Some f -> Bool

(<=) :: Some f -> Some f -> Bool

(>) :: Some f -> Some f -> Bool

(>=) :: Some f -> Some f -> Bool

max :: Some f -> Some f -> Some f

min :: Some f -> Some f -> Some f

ShowF f => Show (Some f)

Defined in Data.Parameterized.Some

Methods

showsPrec :: Int -> Some f -> ShowS

show :: Some f -> String

showList :: [Some f] -> ShowS

HashableF f => Hashable (Some f)

Defined in Data.Parameterized.Some

Methods

hashWithSalt :: Int -> Some f -> Int

hash :: Some f -> Int