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.)