2014-06-13 11:54 GMT+02:00 Roberto Di Cosmo <roberto@dicosmo.org>:

On Fri, Jun 13, 2014 at 11:43:20AM +0200, Gabriel Scherer wrote:
> Encoding integers with addition at the type level is easy enough (it
> is possible to use a technique akin to difference list where you keep
> unary numbers with a unification variable at their tail, to get the
> unification engine to do the addition for you). Anything below that,
> in particular substraction, cannot be done *conveniently* in the
> type-system. It is possible to encode arbitrary operation on
> type-level numbers (unary or not), expressed relationally
> (Prolog-style: ('a, 'b, 'c) add is inhabited if 'a+'b='c) by a GADT
> witnessing the relation, but actually building and using these
> operations then requires the programmer to provide those witness terms
> that are manipulated at runtime.

Actually, we want to have dimension checking at compile time, with no
trace of it at runtime.

Is it possible to think with dimension inference ? This avoid the need to give dimension everywhere.

You can have rules like
if "a + b = c" => dim(a) == dim(b) == dim(c).

if(e*f=g) => dim(g) = dim(e) * dim(f)

You can even go further. https://en.wikipedia.org/wiki/Dimensional_analysis gives some hint : Position vs displacement.

if T1 and T2 are absolut point in time, (T1-T2) are time offset. But "T1 + T2" is a none sense.

You could also extend the check of dimension in space direction (x,y,z).

The idea is to add a check with minimum new user input.

Nicolas