<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On 26 August 2016 at 13:01, Steven D'Aprano <span dir="ltr"><<a href="mailto:steve@pearwood.info" target="_blank">steve@pearwood.info</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span class="">On Fri, Aug 26, 2016 at 07:35:36AM +0200, Pavol Lisy wrote:<br>
> On 8/25/16, Ken Kundert <<a href="mailto:python-ideas@shalmirane.com">python-ideas@shalmirane.com</a>> wrote:<br>
><br>
> [...]<br>
><br>
> > Just allowing the units to be present, even it not<br>
> ><br>
> > retained, is a big advantage because it can bring a great deal of clarity to<br>
> > the<br>
> > meaning of the number. For example, even if the language does not flag an<br>
> > error<br>
> > when a user writes:<br>
> ><br>
> > vdiff = 1mV - 30uA<br>
><br>
> It reminds me: "Metric mishap caused loss of NASA's Mars Climate<br>
> orbiter. It could be nice to have language support helping to avoid<br>
> something similar.</span><br></blockquote><div><br></div><div>[snip]<br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Take v = s/t (velocity equals distance over time). If I write v = s<br>
because it is implicitly understood that the time t is "one":<br>
<br>
s = 100 miles<br>
v = s<br>
<br>
Should v be understood as 100 miles per hour or 100 miles per second or<br>
100 miles per year? That sort of ambiguity doesn't come up in circuit<br>
design, but it is common elsewhere.<br></blockquote></div><br></div><div class="gmail_extra">If one writes this as<br><br></div><div class="gmail_extra">from units import m, s, miles<br></div><div class="gmail_extra"><br></div><div class="gmail_extra">s = miles(100)<br></div><div class="gmail_extra">v: m/s = s<br><br></div><div class="gmail_extra">This could be flagged as an error by a static type checker.<br><br></div><div class="gmail_extra">Let me add some clarifications here:<br></div><div class="gmail_extra">1. By defining __mul__ and __truediv__ on m, s, and other units one can achieve<br></div><div class="gmail_extra">the desirable semantics<br><br></div><div class="gmail_extra">2. Arbitrary (reasonable) unit can be described by a tuple of 7 rational numbers<br></div><div class="gmail_extra">(powers of basic SI units, m/s will be e.g. (1, -1, 0, 0, 0, 0, 0)), if one wants also<br></div><div class="gmail_extra">non SI units, then there will be one more float number in the tuple.<br><br></div><div class="gmail_extra">3. It is impossible to write down all the possible overloads for operations on units,<br>e.g. 1 m / 1 s should be 1 m/s, 1 m/s / 1 s should be 1 m/s**2,<br></div><div class="gmail_extra">and so on to infinity. Only finite number of overloads can be described with PEP 484 type hints.<br><br></div><div class="gmail_extra">4. It is very easy to specify all overloads with very basic dependent types,<br></div><div class="gmail_extra">unit will depend on the above mentioned tuple, and multiplication should be overloaded<br></div><div class="gmail_extra">like this (I write three numbers instead of seven for simplicity):<br></div><div class="gmail_extra"><br></div><div class="gmail_extra">class Unit(Dependent[k,l,m]):<br></div><div class="gmail_extra"> def __mul__(self, other: Unit[ko, lo, mo]) -> Unit[k+ko, l+lo, m+mo]:<br> ...<br><br></div><div class="gmail_extra">5. Currently neither "mainstream" python type checkers nor PEP 484 support dependent types.<br><br></div><div class="gmail_extra">6. For those who are not familiar with dependent types, this concept is very similar to generics.<br></div><div class="gmail_extra">Generic type (e.g. List) is like a "function" that takes a concrete type (e.g. int) and "returns" another<br></div><div class="gmail_extra">concrete type (e.g. List[int], lists of integers). Dependent types do the same, but they allowed to<br></div><div class="gmail_extra">also receive values, not only types as "arguments". The most popular example<br></div><div class="gmail_extra">is matrices of fixed size n by m: Mat[n, m]. The matrix multiplication then could be overloaded as<br><br></div><div class="gmail_extra">class Mat(Dependent[n, m]):<br></div><div class="gmail_extra"> def __matmul__(self, other: Mat[m, k]) -> Mat[n, k]:<br> ...<br></div><div class="gmail_extra"><br>7. I like the formulation by Nick, if e.g. the library circuit_units defines sufficiently many overloads,<br></div><div class="gmail_extra">then it will safely cover 99.9% of use cases *without* dependent types. (An operation<br></div><div class="gmail_extra">for which type checker does not find an overload will be flagged as error, although the operation might be correct).<br></div><div class="gmail_extra"><br>--<br></div><div class="gmail_extra">Ivan<br></div></div>