Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[@tailcall] attribute fails to warn about some stack calls #7525

Closed
vicuna opened this issue May 4, 2017 · 3 comments
Closed

[@tailcall] attribute fails to warn about some stack calls #7525

vicuna opened this issue May 4, 2017 · 3 comments

Comments

@vicuna
Copy link

vicuna commented May 4, 2017

Original bug ID: 7525
Reporter: domsj
Assigned to: @gasche
Status: resolved (set by @gasche on 2017-05-05T14:19:50Z)
Resolution: not a bug
Priority: normal
Severity: minor
Version: 4.03.0
Category: language features

Bug description

example code:

let () =
let x f g =
f ();
g ();
f ();
()
in
let rec inner () =
(inner [@tailcall]) (); (* compiler warns about this )
x
(fun () -> ())
(fun () -> if false then (inner [@tailcall]) ()) (
but wrongly thinks this code is ok? *)
in
inner ()

==============

Encountered this problem when doing a recursive call in an exception handler (e.g. with Lwt.catch)

@vicuna
Copy link
Author

vicuna commented May 4, 2017

Comment author: @gasche

It is not clear to me why you think there is a bug. Within the closure, the inner [@tailcall] () call is a tail call. The closure itself is not called in tail position within x, so if you annotated the g (); call there you would get a warning.

@vicuna
Copy link
Author

vicuna commented May 5, 2017

Comment author: domsj

Let's use Lwt.catch as an example. see https://github.com/ocsigen/lwt/blob/3.0.0/src/core/lwt.ml#L702 for the implementation.
The exception handler (f in the definition there) is not called in tail position, which is perfectly fine.

However when writing a recursive function which uses Lwt.catch I would like ensure that my function only calls itself in a tail recursive way.
I assumed that annotating all recursive calls with [@tailcall] would help me in doing this. And it does so partially, but apparently not when the recursive call happens from within a closure, then the attribute can't give me guarantees about how the function as a whole behaves.

(Even better than annotating all call sites I would like to annotate the function definition with [@tailrec]...)

I suppose there's no attribute to let the compiler help me enforce what I would like to achieve here?

@vicuna
Copy link
Author

vicuna commented May 5, 2017

Comment author: @gasche

The tailcall annotation has a simple, local semantics: it is applied on a call, and results in a warning if the call is not a tailcall.

What you are asking for is different, and there is no simple/modular way to interpret it: as long as a function is passed to a callee instead of called directly -- it is passed as a value, or used in a closure that it itself passed as a value -- you need to reason on the code of that callee to know if it will call its argument in tail-call position, or you need to strengthen the type-system to have a way to track this information across boundaries.

The simplest way to give the guarantee that you want would be to just warn on any use of the recursive function that is not a call in the current expression. But that this extremely restrictive, for example you could not use the @@ or |> operators on a recursive call, of kprintf, etc.

A more expressive way would be to distinguish a type of functions that may only be called in tail position (could be "(a -> b)[@tail]" for example), have the functions above enriched with these richer type annotations, and have something that would warn whether a recursive function is passed as an argument at a type that is not a tail-function type. But this sounds delicate to implement, requires subtyping, breaks principality, and does not interact very well with polymorphism.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants