Data.UnitsOfMeasure.Singleton

This module defines singleton types for integers and concrete units.

Singletons for units

data SUnit u 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 (UnitSyntax Symbol) SUnit

forgetSUnit :: SUnit u -> UnitSyntax String

Extract the runtime syntactic representation from a singleton unit

class KnownUnit u 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 ((:/) Symbol 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 where

Singleton type for lists of base units

Constructors

SNil :: SList []

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

Instances

TestEquality [Symbol] SList

class KnownList xs 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)

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