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

Ignoring principal-type and hints in let-rec bindings #6911

Closed
vicuna opened this issue Jun 20, 2015 · 4 comments
Closed

Ignoring principal-type and hints in let-rec bindings #6911

vicuna opened this issue Jun 20, 2015 · 4 comments
Assignees

Comments

@vicuna
Copy link

vicuna commented Jun 20, 2015

Original bug ID: 6911
Reporter: wieczyk
Assigned to: @gasche
Status: closed (set by @xavierleroy on 2017-02-16T14:15:14Z)
Resolution: not a bug
Priority: low
Severity: minor
Platform: Linux
Version: 4.02.1
Category: typing

Bug description

In this code:
vvvvvvvvvvvvvvvvvvvvvvvvvv
let rec f a =
let id x = x in
1 + g id a

and g (k : 'a -> 'a) a : 'a =
k a

let h k a =
k a
^^^^^^^^^^^^^^^^^^^^^^^^

I would expect that functions 'g' and 'h' have identical type, especially a gave type hints in the definition of the function g.

The type of g is: (int -> int) -> int -> int.

Even if it is desired that functions from 'let-rec' block do not have most general type, but most accurate for this block... then compiler should reject my type hints.

In programming it is a bit annoying that to get most generic type of my code I had to do some hacks like redefine function after let-rec block, or write some more general function before let-rec block.

Steps to reproduce

Just compile my code.

@vicuna
Copy link
Author

vicuna commented Jun 20, 2015

Comment author: @gasche

The semantics of ('a) as a type annotation is not what you think it is. (k : 'a -> 'a) holds if for some type 'a, k has this type -- it does not enforce polymorphism. If you want to enforce polymorphism, use the "Explicit polymorphic type annotations" documented in
http://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec227

and g : 'a . ('a -> 'a) -> _ -> 'a = fun k -> ...

@vicuna
Copy link
Author

vicuna commented Jun 20, 2015

Comment author: wieczyk

Bleh, ugly notation.

One question more:
Does exist a reason why the g function does not get a principal type?

@vicuna
Copy link
Author

vicuna commented Jun 20, 2015

Comment author: @gasche

Inferring polymorphic types for recursive functions is undecidable (because you need to type-check the function body itself with the final type; if you assume that it is monomorphic you can use the usual HM machinery, but there is no way to guess a polymorphic type out of the blue).

In fact the specification of the hindley-milner type system is that it gives monomorphic types to recursive functions (which also makes sense if you think of a "fix" combinator which would naturally be instantiated with a monomorphic type). With this specification, the inference process is principal, as it infers the most general monomorphic type.

(Principality is a relation between an algorithmic inference process and a declarative type system serving as specification.)

It is a relatively recent addition to the language (3.12 was released in 2010) that the users can explicitly decide to put a polymorphic type annotation to recursive functions, effectively widening the space of possible types that can be assigned to a recursive function.

Note that the mistake you made (assuming that type variables would enforce polymorphism) is common enough that it is consensual that there is a problem here that should be solved. But it's unclear what the best solution is, and it is hard to fix design decisions that are this old (this syntax was always part of ML) without breaking existing codebases.

@vicuna
Copy link
Author

vicuna commented Jun 20, 2015

Comment author: wieczyk

Thanks for comment.

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