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)

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

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)

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)