[woolion]

Thank you for your reply. FTR, I find the subject very interesting and I hope there will be more work on this line of approach.

>The problem with those methods is that they're inference time

I agree, I just thought it was missing some prior art (not affiliated with these papers :-P)

What is not clear to me at all is, is this the draft of a research idea? Or is there already some implementation coming in a later post?

It seems to me that such an idea would be workable on a given language with a given type system, but it seems to me there would be a black magic step to train a model that would work in a language-agnostic manner. Could you clarify?

[bgavran]

There is an existing implementation validating this idea, and the plan is to make it publicly available at some point.

> It seems to me that such an idea would be workable on a given language with a given type system, but it seems to me there would be a black magic step to train a model that would work in a language-agnostic manner.

That's correct. The blog post alludes to infrastructure building as a necessary component of making that happen for that exact reason. I.e. while it's "easy" to generate a dependent pair in this way, generating an entire dependently typed AST is much more difficult. On the positive side, this is more of a software engineering effort rather than a research one.

[woolion]

Ok, thank you for the info. Do you have any idea when at some point might be? I'd love to check it out.