aya-dev
aya-dev copied to clipboard
aya-prover
Coercion
random thoughts:
- I believe that coercion is just custom subtyping rules. Am I right?
- Does Arend coercion allow coercing a type with parameters, like
\all {A} {n : Nat} -> Vec A n -> List A? - I don't like Arend's syntax of putting corecion into a
\whereblock. I prefer writing coercion rules as a global definition.
- I believe that coercion is just custom subtyping rules. Am I right?
We might need a more precise definition of "subtyping." For now, I would define coercion as "functions that are implicitly inserted during elabration to make things tyck."
- I don't like Arend's syntax of putting corecion into a
\whereblock. I prefer writing coercion rules as a global definition.
Arend is totally abusing \where blocks! On the other hand, coercion rules might also need some form of scope control.
We might need a more precise definition of "subtyping." For now, I would define coercion as "functions that are implicitly inserted during elabration to make things tyck."
Totally agreed
On the other hand, coercion rules might also need some form of scope control.
Yes. I suggest 'this coercion is accessible by name directly' = 'this coercion is in scope'
Does Arend coercion allow coercing a type with parameters, like \all {A} {n : Nat} -> Vec A n -> List A?
I don't know. I wish we could have that :worried:
Does Arend coercion allow coercing a type with parameters, like \all {A} {n : Nat} -> Vec A n -> List A?
I don't know. I wish we could have that 😟
I think this look interesting and I do not know if any language has this. Arend seems not. Maybe it is somehow novel (in an implementation sense) and can be very powerful.
We have a paper on coercion for HM here: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/icfp051-swamy.pdf
Maybe we can base our DT coercion on it.
One problem to handle is ambiguous coercions. Say one write A -> B and B -> C and A -> C coercions. We will be unable to know which to use when user passes an A to a position of C. A more subtle case is when we have both coercions (x : B) -> A x -> C and A n -> C where n : B constant and we want to coerce a A n to C.
I cannot think of a way better than giving a an error and ask user to resolve the ambiguity manually.
This is totally fine, and that's the reason why we have named coercions, similar to the situation for typeclasses.
And why we need named coercion instances: https://github.com/coq/coq/issues/9275 So another reason for making coercion typeclasses again.
Proposal: don't auto-insert coerce and leave everything to the library.
Rationale:
- Then coercion is totally a library-level thing. So one less language feature (which seems ad-hoc anyway)
- Implicit type-cast might not be a good idea in a language where types play a central role.
The only cost is having to write coerce every time we need it. We can make this name shorter (e.g., _⬇), and the library author can always decide to use {A : Type} {AtoG : Into Group A} (G : A) instead of (G : Group) when that makes more sense. Rust is using this, and in many libraries you can find signatures like fn send<T> (text: T) where T: Into<String>
This way we make our language a bit less like a dynamic one. Not sure if this is good or bad though.
Also we can use the sharp symbol or flat symbol to make our code look more musical
Of course we can first leave the auto coercion insertion unimplemented and decide later... and maybe we can make it optional (by some kind of pragma) in the future.
This way we make our language a bit less like a dynamic one.
Making it look like a dynamic one is not part of our design goal if I recall correctly.
Also we can use the sharp symbol or flat symbol to make our code look more musical
Yes, I think the flat symbol is a reasonable choice.
Making it look like a dynamic one is not part of our design goal if I recall correctly.
Yeah, explicit is better than implicit.
Here is another problem: Should we also make record subtyping explicit? E.g, we have g : Group A and \record Group (A : \Type) \extends Monoid A, should we have g : Monoid A or coerce g : Monoid A?
Making it look like a dynamic one is not part of our design goal if I recall correctly.
But you linked to "Notation Lives Matter" lol
Agda is not able to infer this.
And I think we might need some innovation to solve inference problems for such instances.
Agda is not able to infer this.
Apologies, I think I might have misunderstood Agda's instance mechanism, and I need some time to revise the code. Please ignore my previous comment for now.
Ok, turns out it's the problem with what Agda calls "overlapping instances." If you add OPTIONS --overlapping-instances then the code, well, still doesn't compile and Agda enters an infinite loop.
Upon reading Agda's instance resolution algorithm I think they did something wrong: by using a simple DFS, the resolution process gets trapped in trying to insert more and more intermediate steps (From S T -> From S U, From U T -> From S U, From U V, From V T -> etc.
What we need is a BFS, but that's going to consume too much memory. So maybe we should adopt IDDFS, which is going to guarantee a shortest instance resolution depth.
But again, it's still too early to decide on anything.
Yes, that sounds like some important decisions, but probably would be done after we make structures available
This paper on Lean 4 typeclass resolution seems to claim that it solves this infinite expansion problem.
What we need is a BFS, but that's going to consume too much memory. So maybe we should adopt IDDFS, which is going to guarantee a shortest instance resolution depth.
My guess was right, Agda provides an --instance-search-depth option, and after tuning that to 3 the code actually compiled. But Agda should still use IDDFS for instance resolution.
I'm thinking 'bout this now. We should implement this to make Aya more 'practical'.