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

Methods

testEquality :: f a -> f b -> Maybe ((SUnit :~: 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

Minimal complete definition

unitSing

Methods

unitSing :: SUnit u

Instances

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

Methods

unitSing :: SUnit ((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 :: [Symbol]) 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

Methods

testEquality :: f a -> f b -> Maybe ((SList :~: 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

Minimal complete definition

listSing

Methods

listSing :: SList xs

Instances

KnownList ([] Symbol)

Methods

listSing :: SList [Symbol]

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

Methods

listSing :: SList ((Symbol ': x) xs)