Here is a bidirectional STλC type checker in string diagram Mercury, or something.
Conversation
Yep. I think polarities and determinism annotations are good ideas for logic programming.
1
Ahh cool! Yeah, I've seen some of the Mercury at work, and it's pretty neat what can be done! I'm guessing by "polarity" you mean the "modes" in Mercury? I _think_ we made that connection (currently building a bidirectional type checker for a project).
1