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

[Andreas Abel]

Hi Conor,

sorry that I can only offer sprinkled sentences as a response to your  
elaborate argument. ;-)

On Sep 29, 2010, at 5:03 PM, Conor McBride wrote:
> 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?

Trying rows of hidden arguments would not be a "heuristics" but a  
principled approach.  No clue if something like that would work.

> 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

Coq does not have first-class hidden arguments, and I came to miss  
them during my INRIA adventure last year.  I would not like to give up  
on them...

> 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.

A core language does not need it, and it would of course be nice if it  
could be resolved before type-checking.  If the price ain't too high,  
I am the last to object to a well-specified behavior...

> 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.

Cheers,
Andreas

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/