in which I play around with bidirectional typechecking
pip3 install mypy parsy, then mypy yuki.py and python3 yuki.py
it's very WIP, but one day this kind of thing will typecheck:
(* this is the very cool and good type of integer multiplication in this type system *) (* & is taking the intersection of function types: *) mul : (pos ->pos ->pos ) & (pos ->zero->zero) & (pos ->neg ->neg ) & (zero->pos ->zero) & (zero->zero->zero) & (zero->neg ->zero) & (neg ->pos ->neg ) & (neg ->zero->zero) & (neg ->neg ->pos ) mul = __builtin_mul (* and | is taking the union of value types: *) square : (zero|pos|neg) -> (zero|pos) square = fn x => mul x x
(so, the integer type is a union zero|pos|neg, and we infer from the type of mul that a square is indeed never negative.)