Hey, I was wondering if you had any thoughts about how I might implement a validator for my core syntax, given the presence of metavariables? Eg. github.com/brendanzab/rus - ie. my solutions are value in the meta environment, but I can't get the type of those…
Conversation
You either need to unfold all solved metas in core syntax ("zonking"), or remember types of metas. Neither are too complicated but I prefer the latter, because zonked syntax is cluttered, and typed metas are needed anyway for more sophisticated unification.
1
2
But in the absence of glued evaluation, meta solutions and their types are always greatly bloated.
3
1
Replying to
My plan is to eventually head towards gluing, so yeah, maybe I’ll go with the latter option. Thanks again for all your help!
Would doing the latter option mean that I wouldn’t be able to easily synthesise the type of a hole (a metavariable)? Because then I’d need to know what level of type metavariable is at?
1
I'm not sure about your question, but you always need to return a type when synthesizing a hole, and saving metas doesn't affect this. Hole synthesizing creates at least two metas, one for the hole and one for its type.
1
Show replies