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