search

yeslogic / fathom

🚧 (Alpha stage software) A declarative data definition language for formally specifying binary data formats. 🚧
Apache License 2.0
259 stars 14 forks source link

Implicit function cleanups #453

Closed brendanzab closed 1 year ago

brendanzab commented 1 year ago

Some cleanups to the implementation of implicit functions that were added in #439. I’ve broken the dependency on core::Plicity in the surface syntax, adjusted some names, and cleaned up the insertion of implicit arguments somewhat (inspired by elaboration-zoo’s implementation).

brendanzab commented 1 year ago

Why replace turn surface::Param into an enum? What if we want to add other annotations to parameters, such as erasure?

I guess I still had in my head the {A : Type} -> B syntax, where the “implicitness” is part of the parameter syntax – but as we have said before - this is ambiguous with our record syntax. We could make the erasure annotations fields on the variants… but I do see how it would be a similar problem to implicitness – where we might want to use one of those variants in the surface module? I can re-think that commit if it’s easier.