Date ons 20 november 2019

Units is a well established typecheck that is underused in todays programming worlds. We have famous disasters from using the wrong units, a Mars lander crashed due to such a bug. I think it is a misstake not to have units in the type system of the language. So I asked myself what is the unit functionality that would make me drool. The answer to this is to handle the units as si units with integer exponents and use clpfd to construct constraints on them.

So taking the exponent of a unit value of the format

Value : Unit


We use the tr/2. This function do translate algebraic expressions of units like

?- tr(1:dm,Length).
Length = 0.1 : [1,0,0,0,0,0,0]


We see that we represents the unit as a list of individual SI units exponents, the list is [m,kg,s,A,K,cd,mol]. We can do algebra as well like

?- tr(1:m / 2:s,Velocity).
Velocity = 1 : [1,0,-1,0,0,0,0]


Also we can issue a combined unit and also use common derived units

?- tr(1:'N'*m,Energy).
Energy = 1 : [2,1,-2,0,0,0,0]


We also have the $$===$$ operator. It will unify the algebraic value of lhs and rhs and use clpfd constraint on lhs and rhs of the expression e.g.

'==='(X,Y) :-
tr(X,X1:X2),
tr(Y,Y1:Y2),
X1=Y1,
X2 #= Y2.


A multiplication is translated as

tr(X*Y,Z1:Z2) :-
tr(X,X1:X2),
tr(Y,Y1:Y2),
Z2 #= X2 + Y2,
(number(X1),number(Y1)) -> Z1 is X1 * Y1 ; true).


Exponentiation is translated to:

tr(X**N,Z1:Z2) :-
tr(X,X1:X2),
Z2 #= X2 * N,
(number(N),number(X1)) -> Z1 is X1 ** N ; true).


Sum gives:

tr(X+Y,Z1:Z2) :-
tr(X,X1:X2),
tr(Y,Y1:Y2),
X2 #= Y2,
Z2 #= X2,
(number(X1),number(Y1)) -> Z1 is X1 + Y1 ; true).


With this we can do cool operations as making sure a has no unit

unitexp(X,A,AA,Z) :-
AA = A:_,
XX u= AA*X
equalUnits(XX,1),
Z is exp(XX).

:::prolog
?- unitexp(1:m,2,A,Z).

A = 2 : [-1,0,0,0,0,0,0]
Z = 7.38905609893065 : [0,0,0,0,0,0,0]


The most advanced constraint solving technique one can use is to find pretty printing of units. Sometimes Volt is a better unit than it's SI unit counterpart so we could ask, what is the representation of a unit with the fewest unit symbols? The algorithm I'm using is to first try one symbol then two then three and so on. here is the code for two symbols

try2(X,S1,N1,S2,N2) :-
tr(X,_:Y),
gen(S1),
gen(S2),
S2 \= S1,
tr(1:S1**N1*S2**N2,_:Y),
t([N1,N2])


t/1 is basically a labeling that fails if labels send an exception. gen/1 generates all unit symbols that we allow for the pretty printing and you see how we try to constrain the solution to yield solution values for N1,N2. Here is a demo how it can work (we use pr/1 to pretty print a unit expression):

?- pr(1:'N'*m*s**(-1)).
1:W

?- pr(1:'N'*m*s**(-2)).
1:s**-2 J


We could improve it further if we for example try to find all answers with two units and pick the one with the lowest sum of abolute exponentials. If we implement this we get,

?- pr(1:'N'*m*s**(-2)).
1:s**-1 W


This library works with swi prolog and you can find the source code in the guile-log's source tree (LGPL v2 or v3).

'languge/prolog/modules/example/units.pl'


First use the clpfd module then ensure_load the file and have a play if using swipl.

Using the === operator is as simple as

?- X : km/h === 1 mile/h.
X = 1.609344

X === 1 mile/h.
X = 0.44704:[1, 0, -1, 0, 0, 0, 0].


Also we have constants/2 That can give physical constants with their units.

?- constants(e0,X),pr(X).
8.854187812786998e-18:m**-1 F
X = 8.854187812786998e-18:[-3, -1, 4, 2, 0, 0, 0]


A drawback for a system that handle units is that libraries is harder to write and you could expect that you need to write multiple versoins of the same function. Nah this system is powerful enough to make it generic, have a look at this

limit(Min,Max,X,Y) :- Y === max(Min:_,min(Max:_,X)).

?- limit(1,10,2:m,Y).
Y = 2:[1, 0, 0, 0, 0, 0, 0].

?- limit(1,10,20:m,Y).
Y = 10:[1, 0, 0, 0, 0, 0, 0].

?- limit(1,10,0:m,Y).
Y = 1:[1, 0, 0, 0, 0, 0, 0].


Have fun!!