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

[Ulf Norell]

On Tue, Sep 28, 2010 at 6:05 PM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:

> I looked at the Agda type checker and want to add some clarifications here:
>
> - Bidirectional type checking:  Agda does not do bidirectional checking (=
> type checking and type inference), it only does type checking, where
> checking against a metavar has similar results to type inference.  Still,
> bidirectional type checking is a metaphor that explains some of Agda's
> behavior.
>
> As Nisse already pointed out, typed and untyped lambdas are treated
> differently.
>
>  \ x -> t   expects to be checked against a function type.  If it does not
> get a function type (e.g., it is checked against a meta variable, the type
> checking problem is postponed, but no constraint is propagated that the type
> of \ x -> t must be a function type).
>  This explains the failure of Alan's term x1.
>
>  \ (x : A) -> t  synthesizes a function type (x : A) -> ?B where the new
> meta-var is the type of t
>  @Thorsten: Thus, not all metavars come from holes in the input!
>
> Thus, \ (x : _) and \ x behaved differently, which is unexpected and
> confusing to the outsider.  As we have seen by Alan's examples, there are
> cases where \ (x : _) works and \ x not.  Can it also be the other way
> round?
>
> @Ulf: Could \x be treated as \(x : _) ? There seems to be some abandoned
> code "forcePi" that tried to do this...
>

I can't actually remember why they're treated differently. You could always
change it and see if all the tests pass.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100928/2870cad5/attachment.html