uom-plugin-0.3.0.0: Units of measure as a GHC typechecker plugin

Safe Haskell	None
Language	Haskell2010

Data.UnitsOfMeasure.Singleton

Contents

Singletons for units
Singletons for lists

Description

This module defines singleton types for integers and concrete units.

Synopsis

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

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

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) #