This should evolve into a feature request in time. I just want to record some thoughts.
Consider the situation
and we want to insert not into the hole. It would be great if we could refine it to b = not ?, rather than forcing the user to both insert the global var not and also insert an application node.
There are some choices here, and it interacts with our notion to enforce η-long forms / fully-applied functions. The main decision here is whether to do "the right type-directed thing" or "apply all its argument". For instance, what about
and inserting and: should this give and ? or {? and ? ? ?}?
Everything works fairly straightforwardly for constructors, since they have a rigid return type, but there are many pitfalls for doing this with general polymorphic functions: it may not be obvious how many arguments it has, if you instantiate its type applications with an arrow; doing the "right type-directed thing" is also not obvious to me without needing good type inference etc.
This should evolve into a feature request in time. I just want to record some thoughts.
Consider the situation
and we want to insert
notinto the hole. It would be great if we could refine it tob = not ?, rather than forcing the user to both insert the global varnotand also insert an application node.There are some choices here, and it interacts with our notion to enforce η-long forms / fully-applied functions. The main decision here is whether to do "the right type-directed thing" or "apply all its argument". For instance, what about
and inserting
and: should this giveand ?or{? and ? ? ?}?Everything works fairly straightforwardly for constructors, since they have a rigid return type, but there are many pitfalls for doing this with general polymorphic functions: it may not be obvious how many arguments it has, if you instantiate its type applications with an arrow; doing the "right type-directed thing" is also not obvious to me without needing good type inference etc.