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 #35

Closed LighghtEeloo closed 1 year ago

LighghtEeloo commented 1 year ago

Implements a bidirectional version of the current type-checker with respect to formalism, which only allows analysis for introduction forms and synthesis for elimination forms.

maxsnew commented 1 year ago

Does this implement parameterized datatypes? I don't see any tests for them

LighghtEeloo commented 1 year ago

No it doesn't; the patches are in the parameterized-types branch; which has now been updated.