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