units-2.4.1.2: A domain-specific type system for dimensional analysis

Copyright(C) 2013 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (rae@cs.brynmawr.edu)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Metrology.Z

Contents

Description

This module defines a datatype and operations to represent type-level integers. Though it's defined as part of the units package, it may be useful beyond dimensional analysis. If you have a compelling non-units use of this package, please let me (Richard, rae at cs.brynmawr.edu) know.

Synopsis

The Z datatype

data Z Source #

The datatype for type-level integers.

Constructors

Zero 
S Z 
P Z 
Instances
Eq Z Source # 
Instance details

Defined in Data.Metrology.Z

Methods

(==) :: Z -> Z -> Bool #

(/=) :: Z -> Z -> Bool #

SEq Z => SEq Z Source # 
Instance details

Defined in Data.Metrology.Z

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b) #

(%/=) :: Sing a -> Sing b -> Sing (a /= b) #

PEq Z Source # 
Instance details

Defined in Data.Metrology.Z

Associated Types

type x == y :: Bool #

type x /= y :: Bool #

SDecide Z => SDecide Z Source # 
Instance details

Defined in Data.Metrology.Z

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b) #

SingKind Z Source # 
Instance details

Defined in Data.Metrology.Z

Associated Types

type Demote Z = (r :: Type) #

Methods

fromSing :: Sing a -> Demote Z #

toSing :: Demote Z -> SomeSing Z #

SingI Zero Source # 
Instance details

Defined in Data.Metrology.Z

Methods

sing :: Sing Zero #

SingI n => SingI (S n :: Z) Source # 
Instance details

Defined in Data.Metrology.Z

Methods

sing :: Sing (S n) #

SingI n => SingI (P n :: Z) Source # 
Instance details

Defined in Data.Metrology.Z

Methods

sing :: Sing (P n) #

SuppressUnusedWarnings PSym0 Source # 
Instance details

Defined in Data.Metrology.Z

SuppressUnusedWarnings SSym0 Source # 
Instance details

Defined in Data.Metrology.Z

SingI PSym0 Source # 
Instance details

Defined in Data.Metrology.Z

Methods

sing :: Sing PSym0 #

SingI SSym0 Source # 
Instance details

Defined in Data.Metrology.Z

Methods

sing :: Sing SSym0 #

SingI (TyCon1 S) Source # 
Instance details

Defined in Data.Metrology.Z

Methods

sing :: Sing (TyCon1 S) #

SingI (TyCon1 P) Source # 
Instance details

Defined in Data.Metrology.Z

Methods

sing :: Sing (TyCon1 P) #

data Sing (a :: Z) Source # 
Instance details

Defined in Data.Metrology.Z

data Sing (a :: Z) where
type Demote Z Source # 
Instance details

Defined in Data.Metrology.Z

type Demote Z = Z
type (x :: Z) /= (y :: Z) Source # 
Instance details

Defined in Data.Metrology.Z

type (x :: Z) /= (y :: Z) = Not (x == y)
type (a :: Z) == (b :: Z) Source # 
Instance details

Defined in Data.Metrology.Z

type (a :: Z) == (b :: Z)
type Apply PSym0 (t6989586621679083879 :: Z) Source # 
Instance details

Defined in Data.Metrology.Z

type Apply PSym0 (t6989586621679083879 :: Z) = P t6989586621679083879
type Apply SSym0 (t6989586621679083877 :: Z) Source # 
Instance details

Defined in Data.Metrology.Z

type Apply SSym0 (t6989586621679083877 :: Z) = S t6989586621679083877

data family Sing (a :: k) :: Type #

The singleton kind-indexed data family.

Instances
data Sing (a :: Bool) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Bool) where
data Sing (a :: Ordering) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Ordering) where
data Sing (n :: Nat) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where
data Sing (n :: Symbol) 
Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where
data Sing (a :: ()) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where
data Sing (a :: Z) Source # 
Instance details

Defined in Data.Metrology.Z

data Sing (a :: Z) where
data Sing (a :: Void) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)
data Sing (a :: All) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: All) where
data Sing (a :: Any) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: Any) where
data Sing (b :: [a]) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: [a]) where
  • SNil :: forall a (b :: [a]). Sing ([] :: [a])
  • SCons :: forall a (b :: [a]) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 ': n2)
data Sing (b :: Maybe a) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Maybe a) where
data Sing (b :: Min a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Min a) where
data Sing (b :: Max a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Max a) where
data Sing (b :: First a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: First a) where
data Sing (b :: Last a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Last a) where
data Sing (a :: WrappedMonoid m) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: WrappedMonoid m) where
data Sing (b :: Option a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Option a) where
data Sing (b :: Identity a) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Identity a) where
data Sing (b :: First a) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: First a) where
data Sing (b :: Last a) 
Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: Last a) where
data Sing (b :: Dual a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Dual a) where
data Sing (b :: Sum a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Sum a) where
data Sing (b :: Product a) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Product a) where
data Sing (b :: Down a) 
Instance details

Defined in Data.Singletons.Prelude.Ord

data Sing (b :: Down a) where
data Sing (b :: NonEmpty a) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: NonEmpty a) where
data Sing (b :: Endo a) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: Endo a) where
data Sing (b :: MaxInternal a) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MaxInternal a) where
data Sing (b :: MinInternal a) 
Instance details

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MinInternal a) where
data Sing (c :: Either a b) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: Either a b) where
data Sing (c :: (a, b)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: (a, b)) where
data Sing (c :: Arg a b) 
Instance details

Defined in Data.Singletons.Prelude.Semigroup

data Sing (c :: Arg a b) where
newtype Sing (f :: k1 ~> k2) 
Instance details

Defined in Data.Singletons.Internal

newtype Sing (f :: k1 ~> k2) = SLambda {}
data Sing (b :: StateL s a) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

data Sing (b :: StateL s a) where
  • SStateL :: forall s a (b :: StateL s a) (x :: s ~> (s, a)). Sing x -> Sing (StateL x)
data Sing (b :: StateR s a) 
Instance details

Defined in Data.Singletons.Prelude.Traversable

data Sing (b :: StateR s a) where
  • SStateR :: forall s a (b :: StateR s a) (x :: s ~> (s, a)). Sing x -> Sing (StateR x)
data Sing (d :: (a, b, c)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (d :: (a, b, c)) where
data Sing (c :: Const a b) 
Instance details

Defined in Data.Singletons.Prelude.Const

data Sing (c :: Const a b) where
data Sing (e :: (a, b, c, d)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (e :: (a, b, c, d)) where
data Sing (f :: (a, b, c, d, e)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (f :: (a, b, c, d, e)) where
  • STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing ((,,,,) n1 n2 n3 n4 n5)
data Sing (g :: (a, b, c, d, e, f)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (g :: (a, b, c, d, e, f)) where
  • STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing ((,,,,,) n1 n2 n3 n4 n5 n6)
data Sing (h :: (a, b, c, d, e, f, g)) 
Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (h :: (a, b, c, d, e, f, g)) where
  • STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f) (n7 :: g). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing n7 -> Sing ((,,,,,,) n1 n2 n3 n4 n5 n6 n7)

type SZ = (Sing :: Z -> Type) Source #

Defunctionalization symbols (these can be ignored)

data SSym0 :: (~>) Z Z Source #

Instances
SuppressUnusedWarnings SSym0 Source # 
Instance details

Defined in Data.Metrology.Z

SingI SSym0 Source # 
Instance details

Defined in Data.Metrology.Z

Methods

sing :: Sing SSym0 #

type Apply SSym0 (t6989586621679083877 :: Z) Source # 
Instance details

Defined in Data.Metrology.Z

type Apply SSym0 (t6989586621679083877 :: Z) = S t6989586621679083877

type SSym1 (t6989586621679083877 :: Z) = S t6989586621679083877 Source #

data PSym0 :: (~>) Z Z Source #

Instances
SuppressUnusedWarnings PSym0 Source # 
Instance details

Defined in Data.Metrology.Z

SingI PSym0 Source # 
Instance details

Defined in Data.Metrology.Z

Methods

sing :: Sing PSym0 #

type Apply PSym0 (t6989586621679083879 :: Z) Source # 
Instance details

Defined in Data.Metrology.Z

type Apply PSym0 (t6989586621679083879 :: Z) = P t6989586621679083879

type PSym1 (t6989586621679083879 :: Z) = P t6989586621679083879 Source #

Conversions

zToInt :: Z -> Int Source #

Convert a Z to an Int

szToInt :: Sing (z :: Z) -> Int Source #

Convert a singleton Z to an Int.

Type-level operations

Arithmetic

type family Succ (z :: Z) :: Z where ... Source #

Add one to an integer

Equations

Succ Zero = S Zero 
Succ (P z) = z 
Succ (S z) = S (S z) 

type family Pred (z :: Z) :: Z where ... Source #

Subtract one from an integer

Equations

Pred Zero = P Zero 
Pred (P z) = P (P z) 
Pred (S z) = z 

type family Negate (z :: Z) :: Z where ... Source #

Negate an integer

Equations

Negate Zero = Zero 
Negate (S z) = P (Negate z) 
Negate (P z) = S (Negate z) 

type family (a :: Z) #+ (b :: Z) :: Z where ... infixl 6 Source #

Add two integers

Equations

Zero #+ z = z 
(S z1) #+ (S z2) = S (S (z1 #+ z2)) 
(S z1) #+ Zero = S z1 
(S z1) #+ (P z2) = z1 #+ z2 
(P z1) #+ (S z2) = z1 #+ z2 
(P z1) #+ Zero = P z1 
(P z1) #+ (P z2) = P (P (z1 #+ z2)) 

type family (a :: Z) #- (b :: Z) :: Z where ... infixl 6 Source #

Subtract two integers

Equations

z #- Zero = z 
(S z1) #- (S z2) = z1 #- z2 
Zero #- (S z2) = P (Zero #- z2) 
(P z1) #- (S z2) = P (P (z1 #- z2)) 
(S z1) #- (P z2) = S (S (z1 #- z2)) 
Zero #- (P z2) = S (Zero #- z2) 
(P z1) #- (P z2) = z1 #- z2 

type family (a :: Z) #* (b :: Z) :: Z where ... infixl 7 Source #

Multiply two integers

Equations

Zero #* z = Zero 
(S z1) #* z2 = (z1 #* z2) #+ z2 
(P z1) #* z2 = (z1 #* z2) #- z2 

type family (a :: Z) #/ (b :: Z) :: Z where ... Source #

Divide two integers

Equations

Zero #/ b = Zero 
a #/ (P b') = Negate (a #/ Negate (P b')) 
a #/ b = ZDiv b b a 

sSucc :: Sing z -> Sing (Succ z) Source #

Add one to a singleton Z.

sPred :: Sing z -> Sing (Pred z) Source #

Subtract one from a singleton Z.

sNegate :: Sing z -> Sing (Negate z) Source #

Negate a singleton Z.

Comparisons

type family (a :: Z) < (b :: Z) :: Bool where ... Source #

Less-than comparison

Equations

Zero < Zero = False 
Zero < (S n) = True 
Zero < (P n) = False 
(S n) < Zero = False 
(S n) < (S n') = n < n' 
(S n) < (P n') = False 
(P n) < Zero = True 
(P n) < (S n') = True 
(P n) < (P n') = n < n' 

type family NonNegative z :: Constraint where ... Source #

Check if a type-level integer is in fact a natural number

Equations

NonNegative Zero = () 
NonNegative (S z) = () 

Synonyms for certain numbers

type One = S Zero Source #

type Two = S One Source #

type Three = S Two Source #

type Five = S Four Source #

type MOne = P Zero Source #

type MTwo = P MOne Source #

sZero :: Sing Zero Source #

This is the singleton value representing Zero at the term level and at the type level, simultaneously. Used for raising units to powers.

sThree :: Sing (S (S (S Zero))) Source #

sFour :: Sing (S (S (S (S Zero)))) Source #

sFive :: Sing (S (S (S (S (S Zero))))) Source #

sMFour :: Sing (P (P (P (P Zero)))) Source #

sMFive :: Sing (P (P (P (P (P Zero))))) Source #

Deprecated synonyms

pZero :: Sing Zero Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pOne :: Sing (S Zero) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pTwo :: Sing (S (S Zero)) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pThree :: Sing (S (S (S Zero))) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pFour :: Sing (S (S (S (S Zero)))) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pFive :: Sing (S (S (S (S (S Zero))))) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pMOne :: Sing (P Zero) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pMTwo :: Sing (P (P Zero)) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pMThree :: Sing (P (P (P Zero))) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pMFour :: Sing (P (P (P (P Zero)))) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pMFive :: Sing (P (P (P (P (P Zero))))) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pSucc :: Sing z -> Sing (Succ z) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pPred :: Sing z -> Sing (Pred z) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.