How abstraction and application are type-checked [Re: [Agda] Agda
type inference oddity on functions]
Andreas Abel
andreas.abel at ifi.lmu.de
Tue Sep 28 22:54:17 CEST 2010
On Sep 28, 2010, at 10:12 PM, Alan Jeffrey wrote:
>> Any ideas how to express the hidden argument stuff as constraints?
>
> If I was building the thing from the ground up, I'd make hidden
> arguments part of functions, that is the primitive type is:
>
> {x : T} (y : U) -> V
>
> with matching lambda and application syntax. The main reason for
> this is to make explicit when hidden arguments are being resolved,
> e.g. you'd have:
>
> nil : {A : Set} -> () -> (List A)
>
> and you could distinguish between:
>
> nil -- still generic
> nil() -- has been made monomorphic
>
> Currently, it's a complete mystery exactly when hidden arguments are
> inserted. Of course, this is completely non-backwards compatible,
> so will probably have to go on the shelf.
>
> The slightly more compatible version would have to be a horrible
> hack, something like as follows...
>
> First, distinguish syntactically between terms with and without
> implicit arguments:
>
> A, B, C ::= lambda [x] . A' | x | A' B | _
> A', B', C' ::= lambda x . A | A [B] | Pi(x:A')B' | Pi[x:A']B' | ...
>
> Here writing [...] for implicit arguments, as we need to do some
> horrid uncurrying to get from the surface {...} to the internal [...]:
>
> \ {x} -> A =def= lambda [(x,y)] . A [y]
> \ x -> A =def= lambda [()] . lambda x . A
> A B =def= A [_] B
> A {B} =def= lambda [x] . A [(B,x)]
> ...
>
> etc. At this point, we can conflate implicit and explicit
> arguments, and do regular old constraint solving.
>
> All quite horrid, but I suspect any attempt to try to make this
> nicer ends up introducing things like row expressions, row
> variables, row metavariables, etc. etc.
Mmh, but that seems more promising than your "horrid" ;-) proposal.
With row variables, an unknown function type would be
{r : ?R} -> (x : ?X) -> ?Y r x
where r is a variable of row type and ?R is a row type metavariable.
Has anyone tried this?
>> On Sep 28, 2010, at 7:43 PM, Alan Jeffrey wrote:
>>
>>> Looks like I'm treading into dangerous water here...
>>>
>>> On 09/28/2010 12:12 PM, Andreas Abel wrote:
>>>> I found an example where untyped lambda succeeds but typed lambda
>>>> fails:
>>>
>>> Oh my goodness. Er, doesn't this mean there's a horrible race
>>> condition in the unification engine? For example, swapping the
>>> order of arguments to foo' gives:
>>>
>>> foo'' : ({X : Set1} -> X == IdT -> X -> Set) -> Set
>>> foo'' k = k refl (\ (x : _) -> x) -- succeeds
>>>
>>> which looks to me that the order of constraint evaluation is making
>>> a difference, so constraint solving isn't Church-Rosser!
>>>
>>> A.
>>>
>>>> module HiddenLambdaInsertion where
>>>>
>>>> IdT = ({A : Set} -> A -> A)
>>>>
>>>> data _==_ {A : Set2}(a : A) : A -> Set where
>>>> refl : a == a
>>>>
>>>> foo : ({X : Set1} -> X -> X == IdT -> Set) -> Set
>>>> foo k = k (\ x -> x) refl -- succeeds
>>>>
>>>> foo' : ({X : Set1} -> X -> X == IdT -> Set) -> Set
>>>> foo' k = k (\ (x : _) -> x) refl -- fails
>>>>
>>>> foo succeeds because type checking \ x -> x : X is postponed
>>>> first
>>>> and can then, after X := IdT, insert a hidden lambda \ {X} before \
>>>> x.
>>>>
>>>> foo' fails because the type of \ (x : _) -> x is inferred as ?X -
>>>>> ?X
>>>> which cannot be unified with {A : Set} -> A -> A.
>>>>
>>>> So typed and untyped lambda cannot be unified into one concept
>>>> unless
>>>> we find a better heuristics of inserting hidden arguments and
>>>> hidden
>>>> abstractions.
>>>>
>>>> @Alan: short response below.
>>>>
>>>> On Sep 28, 2010, at 6:38 PM, Alan Jeffrey wrote:
>>>>
>>>>> Thanks for going through the typechecker Andreas!
>>>>>
>>>>> On 09/28/2010 11:05 AM, Andreas Abel wrote:
>>>>> [...]
>>>>>> 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?
>>>>>
>>>>> It certainly is confusing :-) I'd be surprised if there were
>>>>> cases
>>>>> the other way round, as (AFAICT) \x just propogates fewer
>>>>> constraints then \x:_ -- but then the typechecker always has
>>>>> surprises for me!
>>>>>
>>>>>> @Ulf: Could \x be treated as \(x : _) ? There seems to be some
>>>>>> abandoned code "forcePi" that tried to do this...
>>>>>
>>>>> This would be very nice!
>>>>>
>>>>> [...]
>>>>>> So, can we improve on the type checking of an application f a?
>>>>>> Well if f is not yet known to be a function type, we cannot
>>>>>> simply
>>>>>> say
>>>>>> that it should be (x : ?1) -> ?2 x, where ?1 is the type of a,
>>>>>> because
>>>>>> there might be omitted hidden arguments between f and a. So it
>>>>>> would be
>>>>>>
>>>>>> Delta -> (x : ?1 Delta) -> ?2 Delta x
>>>>>>
>>>>>> where Delta is a telescope of hidden variables of unknown length.
>>>>>
>>>>> Hmm, do we really need to do this? Can we not just say that in an
>>>>> application A B we add the typings:
>>>>>
>>>>> A : (x : ?1) -> (?2 x)
>>>>> B : ?1
>>>>>
>>>>> This doesn't preclude A having hidden arguments, won't they get
>>>>> resolved in the "usual fashion"? A parallel example is something
>>>>> like (A ++ B) which adds the typings:
>>>>>
>>>>> A : List ?1
>>>>> B : List ?1
>>>>>
>>>>> Now if later we discover that A actually has type {T} -> List U
>>>>> then
>>>>> inferred arguments are added, replacing this occurrence of A, and
>>>>> getting:
>>>>>
>>>>> A {?2} : List U
>>>>> B : List U
>>>>> ?2 : T
>>>>
>>>> Well, I doubt it works like this, I would rather expect to get a
>>>> type
>>>> error, because
>>>>
>>>> List ?1 != {T} -> List U
>>>>
>>>>> I must be missing something, why won't the same hidden-argument
>>>>> resolution work for function application?
>>>>
>>>> Hidden Pi-abstractions are never inserted, and the inserting of
>>>> hidden
>>>> arguments and abstractions follows also a fragile heuristics.
>>>>
>>>>>> Such a concept does not exist (yet) in the guts of Agda, so I
>>>>>> guess
>>>>>> the situation cannot be rectified easily.
>>>>>>
>>>>>> Cheers,
>>>>>> Andreas
>>>>>
>>>>> A.
>>>>>
>>>>>>
>>>>>>
>>>>>> On Sep 28, 2010, at 4:06 PM, Alan Jeffrey wrote:
>>>>>>
>>>>>>> On 09/28/2010 05:05 AM, Thorsten Altenkirch wrote:
>>>>>>>>>>> Attached is a program that defines a function whose only
>>>>>>>>>>> effect is
>>>>>>>>>>> to enforce that its argument is a function. The version in
>>>>>>>>>>> the
>>>>>>>>>>> file
>>>>>>>>>>> is level-polymorphic and deals with dependent functions, but
>>>>>>>>>>> its
>>>>>>>>>>> simpler cousin is:
>>>>>>>>>>>
>>>>>>>>>>> isFun : {A B : Set} -> (A -> B) -> (A -> B)
>>>>>>>>>>> isFun f = f
>>>>>>>>>>>
>>>>>>>>>>> Then we can show that there are contexts such that:
>>>>>>>>>>>
>>>>>>>>>>> a) isFun (lambda x -> x) type-infers, but (lambda x ->
>>>>>>>>>>> x) does
>>>>>>>>>>> not.
>>>>>>>>>>
>>>>>>>>>> What does "type-infers" mean?
>>>>>>>>>
>>>>>>>>> I mean "accepted by the Agda type-checker without unsolved
>>>>>>>>> metas",
>>>>>>>>> or
>>>>>>>>> more concretely no yellow ink in agda-mode.
>>>>>>>>
>>>>>>>> I guessed that you mean that it successfully infers a type
>>>>>>>> using
>>>>>>>> C-c
>>>>>>>> C-d. isFun (lambda x -> x) certainly has unresolved metas.
>>>>>>>
>>>>>>> Yes, but the odd thing is we can find a context C s.t. C[lambda
>>>>>>> x ->
>>>>>>> x] has unsolved metas, but C[isFun(lambda x -> x)] does not.
>>>>>>>
>>>>>>> NAD says this is due to a planned future addition to Agda -- not
>>>>>>> every lambda will have function type (and ditto not every
>>>>>>> application will be of a function).
>>>>>>>
>>>>>>> [...]
>>>>>>>
>>>>>>>>> In the example, they're variables, of rather weird type. The
>>>>>>>>> type
>>>>>>>>> of f is:
>>>>>>>>>
>>>>>>>>> {b : bool} -> (F b)
>>>>>>>>>
>>>>>>>>> where:
>>>>>>>>>
>>>>>>>>> F true = (Nat -> Nat)
>>>>>>>>> F false = Nat
>>>>>>>>>
>>>>>>>>> So the oddness is that (isFun f x) is inferred correctly to be
>>>>>>>>> (isFun
>>>>>>>>> (f {true}) x), but (f x) ends up as (f {Z} x) for an unsolved
>>>>>>>>> meta
>>>>>>>>> Z.
>>>>>>>>> AFAICT this is because the inference algorithm doesn't infer a
>>>>>>>>> function type for f, even though it's been applied!
>>>>>>>>
>>>>>>>> I am rather surprised that (isFun f x) can be inferred. Can
>>>>>>>> somebody
>>>>>>>> explain to me why this is the case.
>>>>>>>
>>>>>>> It's because F is a constructor-headed function, so the term
>>>>>>> inference algorithm deduces that F is invertable. So once
>>>>>>> there's a
>>>>>>> constraint (F X == Y -> Z), this is enough to solve (X ==
>>>>>>> true) and
>>>>>>> hence (Y == Z == Nat).
>>>>>>>
>>>>>>> This trick is enough to code functions whose implicit arguments
>>>>>>> have
>>>>>>> default value in existing Agda, if only application
>>>>>>> constrained a
>>>>>>> term to be a function!
>>>>>>>
>>>>>>>> Cheers,
>>>>>>>> Thorsten
>>>>>>>
>>>>>>> A.
>>>>>>> _______________________________________________
>>>>>>> Agda mailing list
>>>>>>> Agda at lists.chalmers.se
>>>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>>>>
>>>>>>
>>>>>> 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/
>>>>>>
>>>>>
>>>>>
>>>>
>>>> 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/
>>>>
>>>
>>>
>>
>> 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/
>>
>
>
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/
More information about the Agda
mailing list