search

zydeco-lang / zydeco

a proof-of-concept programming language based on Call-by-push-value
Other
49 stars 3 forks source link

Bidirectional Type Checking #32

Closed maxsnew closed 1 year ago

maxsnew commented 1 year ago

As discussed in #31 , parameterized data and codata types both would be a lot nicer with a bidirectional type system.

Currently, all forms are synthesizing and all variables need annotations when they are introduced. There are a few hacks because of this currently that will be resolved: for instance empty match statements need to be checking forms.

Let's work on this on the branch https://github.com/zydeco-lang/zydeco/tree/parameterized-types.

LighghtEeloo commented 1 year ago

Maybe Runze and I can take care of this one? Had some ideas for refactoring the type checker for a long time.

P.S. since the repo is now public it should be able to allow multiple assignees.

maxsnew commented 1 year ago

@LighghtEeloo Is there something blocking this getting merged into main?

LighghtEeloo commented 1 year ago

My poor memory made me overlook the fact that the main branch still exists as the default branch for development. Let's do the merge.