At start-up defs that DON'T type check are permitted (so you can use e.g.
loop, map, etc.) in the definitions "source", but then the user-facing
inscribe command only allows you to define new commands that DO
type-check. The ideal solution here is to get inference working for the
loopy words. (In the meantime you can select and execute their
definition text directly. That's not (yet!) type-checked.)
Type checking e.g. sum or product.
Any type accepts complex numbers.
Lots of the math functions now just use Number rather than more specific
poly-types.
Now the UI highlights commands and numbers as you move the mouse, numbers
are blue, commands that type-check are green, commands that fail to
type-check are orange and will not be interpreted, and if there is no
stack effect information available for a command it is grey but you can
still attempt to execute it.
You can still evaluate whole expressions by selceting them and
right-inter-clicking before you release the left button, or by putting
the cursor on a line and typing ctrl-enter, which will run the whole
line. These expressions are NOT (yet) type-checked.
If type vars get into the espression you have to keep them in sync with
the unification or you can lose information.
Some combinators can put symbols on the expression, you have to convert
those to type checkers or, as a hack, just look them up and run them.
This lets definitions work(-ish), ...
It forces the identities of lits to change during relabel().
I think we still have to update() the expression to track changes in the
F function stack effect or we risk losing assoviations between type
variables in the stack effects and type variables in the pending
expression. Hrmmm.
So they can notice if they're given a stack that doesn't match what
they're expecting.
This seems to work, but I realized that type variables in the pending
expression need to be update()'d too. hmm...
Simon Forman