<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><blockquote type="cite"><div><blockquote type="cite"><blockquote type="cite">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:<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> isFun : {A B : Set} -> (A -> B) -> (A -> B)<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"> isFun f = f<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">Then we can show that there are contexts such that:<br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite"><br></blockquote></blockquote><blockquote type="cite"><blockquote type="cite">a) isFun (lambda x -> x) type-infers, but (lambda x -> x) does not.<br></blockquote></blockquote><blockquote type="cite"><br></blockquote><blockquote type="cite">What does "type-infers" mean?<br></blockquote><br>I mean "accepted by the Agda type-checker without unsolved metas", or more concretely no yellow ink in agda-mode.<br></div></blockquote><div><br></div><div>I guessed that you mean that it successfully infers a type using C-c C-d. isFun (lambda x -> x) certainly has unresolved metas.</div><div><br></div><blockquote type="cite"><div><blockquote type="cite">Which type should (lambda x -> x) infer to?<br></blockquote><br>In this example, I was expecting the type inference algorithm to introduce a new meta, and give (lambda x -> x) the type (X -> X). In the example code, that's enough information for the rest of the program to typecheck.<font class="Apple-style-span" color="#000000"><font class="Apple-style-span" color="#144FAE"><br></font></font></div></blockquote><div><br></div><div>I'd say that all the metavariables should come from terms which are left out in user programs. At least this is my understanding of type inference for languages like Agda.</div><div><br></div><div>It is sort of wrong to call Agda's elaboration, type-inference. In my view it should be called term inference, because what is inferred are terms which are left out by the user. These may happen to be types. I think this is a fundamentally different approach to typing then the one taken in conventional languages like Haskell even though it superficially looks similar.</div><div><br></div><div>Having said this, I am sure that there are odd bits in the actual implementation of Agda's elaboration, e.g.</div><div><br></div><div><blockquote type="cite">In the example, they're variables, of rather weird type. The type of f is:<br><br> {b : bool} -> (F b)<br><br>where:<br><br> F true = (Nat -> Nat)<br> F false = Nat<br><br>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!</blockquote><br></div><div>I am rather surprised that (isFun f x) can be inferred. Can somebody explain to me why this is the case.</div><div><br></div><div>Cheers,</div><div>Thorsten</div></div></body></html>