[kpgiskpg]

(Author here).

Here's a not-so-mathy application that I had recently. I was implementing a units system in Python. Operator overloading allowed me to define joules like so: `J = KG * M**-1 * S**-2`. Then I could define grays (a radiation-related unit) like `Gy = J/KG`. Repeat for hundreds of units. If I had to do it in Java, I'd be frustrated by the verbosity and it would be easier to make mistakes.

My point -- Guy's point, actually -- is that if you don't give people the ability to grow a language, then their expressive power will be limited. And you can't anticipate ahead of time all the ways they'll want to express themselves.

Admittedly, my application is kinda mathy under the hood, because the units exist in a vector space. I guess that's to be expected when the operators come from maths.

[schoen]

> Operator overloading allowed me to define joules like so: `J = KG * M*-1 * S*-2`. Then I could define grays (a radiation-related unit) like `Gy = J/KG`. Repeat for hundreds of units.

Presumably exponentiation rather than multiplication by a constant, right?

This is cool and reminds me of how the Python Z3 binding uses operator overloading to let you express arithmetic and logical constraints

  >>> import z3
  >>> s = z3.Solver()
  >>> a, b, c, d = (z3.Int(x) for x in "abcd")
  >>> s.add(a*b == c+d)
  >>> s.add(a+b == c+d)
  >>> s.add(a!=0,b!=0,c!=0,d!=0)
  >>> s.check()
  sat
  >>> s.model()
  [d = 6, c = -2, b = 2, a = 2]
  >>> s.reset()
  >>> s.add(a>1, b>1, c>1)
  >>> s.add(a*a + b*b == c*c)
  >>> s.check()
  sat
  >>> s.model()
  [c = 17, b = 8, a = 15]

(It's limited in some ways for some reasons, like for some types and relations you may have to use a Z3 function to express a relation even though Python has syntax for it -- the example that I know of is that you have to use z3.Or(), z3.And(), etc., with boolean variables instead of Python's builtin boolean operators. Not sure why.)*

[kpgiskpg]

Oh wait, Hackernews seems to have removed one of the astericks symbols. It should be Python's exponentiation operator (2 astericks symbols), ya. (edit: fixed now).

That's cool too! How do you define the variables?

[schoen]

Oh wait, I left that part out! I'll edit my post.

... there we go.

You use Z3 objects that represent unknowns of particular types, like Z3.Int, Z3.Bool, etc. Each one returns an object representing a variable of that type, which can then be used in (Python-formatted!) expressions that you give to a solver.