Brandon T. Willard
Brandon T. Willard
This PR introduces a simple relational typing example for Python AST. This implementation is based on Racket examples provided by @jasonhemann. - [ ] Add all function body statements to...
With `condp` from #48, we could implement a simple, usable version of Pie as a demo of a type system with minimal dependent typing.
This project needs type annotations and a Mypy `pre-commit` hook.
We might want a non-`cons` constraint. It would be a nice way to simplify the specification of some graph/term-walking goals.
We could implement a version of `__setitem__` in the miniKanren state object/mappings (e.g. `ConstrainedState`) that checks constraints immediately after being added to the state. A failure could throw an exception...
`buildo` (soon to be replaced by `applyo`) will actually apply a rator to its rands and unify the result with its third argument: i.e. `buildo(add, (1, 1), q_lv)` should unify...
Needing to add extra `isinstanceo` goals for additional types (e.g. `isinstanceo(x, int), isinstanceo(x, float)` instead of `isinstanceo(x, (int, float))`) is pretty inconvenient (and somewhat wasteful).
We should consider implementing [`__length_hint__`](https://www.python.org/dev/peps/pep-0424/) for goal and state streams. That way, one could make informed, dynamic decisions about computational costs and potentially make better decisions about goal evaluation order.
This isn't a problem in the `neq` constraint, but it's a confusing ambiguity/gotcha that arises from `cons`'s "null" value for lists being both `[]` and `None` (i.e. `cons(1, []) ==...
We could do less collection copying between `ConstrainedState.post_unify_checks` and `ConstraintStore.post_unify_check`. Furthermore, the whole interface could be refactored to return updated constraints.