How abstraction and application are type-checked [Re: [Agda]
Agda type inference oddity on functions]
Alan Jeffrey
ajeffrey at bell-labs.com
Tue Sep 28 23:58:31 CEST 2010
The problem with row variables is that it's very tempting to try to
solve them up to associativity of row composition, for example. lets say
you end up with a constraint:
\{ r1 :?R1 } -> ?A1 : { r2 : ?R2 } -> ?T1
One might think that we should just unify R1 and R2, but what if a later
unification results in:
?A1 = \{ r3 : ?R3 } -> ?A2
If this is allowed (that is, we don't stratify between
allowed-to-have-hidden-arguments types, and
not-allowed-to-have-hidden-arguments types) then all you can deduce
initially about R1 and R2 is that either R1 is a prefix of R2 or vice
versa. You also get fun cases like:
\{ r1 : ?R1 } -> \{ r2 : ?R2 } -> Nat
== \{ r3 : ?R3 } -> \{ r4 : ?R4 } -> Nat
at which point all you know is that:
R1 ++ R2 == R3 ++ R4
Assuming we don't want to have to solve constraints up to associativity,
I suspect the thing to do is to stratify, at which point you can either
deal with row variables or uncurry the rows into nested product types.
The former is probably more elegant, but introduces new machinery; the
latter is hacky, but requires no extensions to the language.
A.
On 09/28/2010 03:54 PM, Andreas Abel wrote:
>
> 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