How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]

[Conor McBride]

Hi

On 28 Sep 2010, at 18:12, Andreas Abel wrote:

>
> So typed and untyped lambda cannot be unified into one concept  
> unless we find a better heuristics of inserting hidden arguments and  
> hidden abstractions.

Now I'm really scared. Why should "heuristics" come into it?

I have been arguing for some time that {x : S} -> T should
not be a type, because it makes constraint-solving too hard
to understand. I got bitten by these problems in Epigram 1
and I believe I said as much some years ago at Agda meetings
and/or Ulf's defence.

This url records some of the discussion:

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.ImplicitSyntax

My proposal was to allow the association of "type schemes"
with variables and definitions in scope, determining their
implicit-versus-explicit conventions. One should need only
identify the function symbol being applied (or for overloaded
constructors, the datatype as well) to determine the
correct positioning of implicit arguments and lambdas.

In Epigram 2, the plan (only partially realised so far) is
to support implicit syntax as an elaboration convention
outside the evidence language, rather than as a funny Pi-type
in the language at any layer.

Inferring the presence or absence of implicit arguments,
together with the dependency of other arguments upon them
offers far more degrees of freedom than can sanely be resolved
from the constraints available. Defaulting heuristics result
in incorrect early commitments as seen in these bugs.

I recommend anxiety as the appropriate state of mind when
designing systems of telepathy.

All the best

Conor