search

diprism / perpl

The PERPL Compiler
MIT License
10 stars 5 forks source link

Consider bidirectional typing? #17

Closed colin-mcd closed 2 years ago

colin-mcd commented 2 years ago

Type checking = does this term have this particular type? Type synthesis = what is the type of this term? Currently, we just do type synthesis (and of course check for type errors and all that). If we do bidirectional typing (checking in some situations and synthesizing in others), it would allow us to cut out the annoying lambda annotations in most situations.

davidweichiang commented 2 years ago

Can you work out what the rules would be? Is this like intermediate between what we have now and full type inference?

colin-mcd commented 2 years ago

I've implemented it before for a much more complex language w.r.t. its type system (dependently typed / higher order), and this would basically just be a subset of the rules for that. I think it'd be pretty easy and straightforward, and make writing programs much nicer.

It's not really much in terms of type inference, because you never need to solve for any unknowns. All this does is allows you to kinda conditionally switch between bottom-up and top-down typing so to speak, depending on how many type annotations the user supplied.