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
My plan is to eventually head towards gluing, so yeah, maybe I’ll go with the latter option. Thanks again for all your help!
1
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
It’s the second one I’m interested in: what type do I give it in the metavariable environment? I have universe levels, so I can’t just use it `Type`
1
1
Oh right. Unfortunately, you need one more meta for the level (yeah levels are painful). In Agda, levels are handled like any other term and have type Set-omega. I *think* in Idris there's a separate metacontext just for levels.
1
1
Replying to
Hehe, oh dear... yeah I was hoping to avoid fancy level unification :3. Hum. Interesting! Will have a think about this!
Replying to
If you don't have cumulativity, level polymorphism and level bounds, then level unification can stay dumb and simple (contrast Agda/Coq level solving), but then it's annoying to use. Why not go with type-in-type?
1
3
Idris maintains a graph of level constraints then solves later, which is a bit of a pain. For a programming language (rather than theorem prover) I don't think type-in-type loses enough to worry about. Though others may argue with this...
2
6
Show replies