But in the absence of glued evaluation, meta solutions and their types are always greatly bloated.
Conversation
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
Hehe, oh dear... yeah I was hoping to avoid fancy level unification :3. Hum. Interesting! Will have a think about this!
1
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
What in particular were you interested in learning about?
level { "solving", "unification" },
why and how much it is needed,
how it works
1
Are you interested in these in relation to dependent type system implementation? You can get by without unification (see Dhall), but it means you have to be more explicit. Doing stuff like `id String "hello"` can get annoying after a while.
1
Show replies