Data.UnitsOfMeasure.Singleton

This module defines singleton types for integers and concrete units.

Singletons for units

data SUnit (u :: UnitSyntax Symbol) where

Singleton type for concrete units of measure represented as lists of base units

Constructors

SUnit :: SList xs -> SList ys -> SUnit (xs :/ ys)

Instances

TestEquality SUnit

Defined in Data.UnitsOfMeasure.Singleton

Methods

testEquality :: forall (a :: k) (b :: k). SUnit a -> SUnit b -> Maybe (a :~: b)

forgetSUnit :: SUnit u -> UnitSyntax String

Extract the runtime syntactic representation from a singleton unit

class KnownUnit (u :: UnitSyntax Symbol) where

A constraint KnownUnit u means that u must be a concrete unit that is statically known but passed at runtime

Methods

unitSing :: SUnit u

Instances

(KnownList xs, KnownList ys) => KnownUnit (xs ':/ ys)

Defined in Data.UnitsOfMeasure.Singleton

Methods

unitSing :: SUnit (xs ':/ ys)

unitVal :: forall proxy u. KnownUnit u => proxy u -> UnitSyntax String

Extract the runtime syntactic representation of a KnownUnit

testEquivalentSUnit :: SUnit u -> SUnit v -> Maybe (Pack u :~: Pack v)

Test whether two SUnits represent the same units, up to the equivalence relation. TODO: this currently uses unsafeCoerce, but in principle it should be possible to avoid it.

Singletons for lists

data SList (xs :: [Symbol]) where

Singleton type for lists of base units

Constructors

SNil :: SList '[]

SCons :: KnownSymbol x => proxy x -> SList xs -> SList (x ': xs)

Instances

TestEquality SList

Defined in Data.UnitsOfMeasure.Singleton

Methods

testEquality :: forall (a :: k) (b :: k). SList a -> SList b -> Maybe (a :~: b)

class KnownList (xs :: [Symbol]) where

A constraint KnownList xs means that xs must be a list of base units that is statically known but passed at runtime

Methods

listSing :: SList xs

Instances

KnownList ('[] :: [Symbol])

Defined in Data.UnitsOfMeasure.Singleton

Methods

listSing :: SList '[]

(KnownSymbol x, KnownList xs) => KnownList (x ': xs)

Defined in Data.UnitsOfMeasure.Singleton

Methods

listSing :: SList (x ': xs)