Type inference vs pointfree style

Learning
,
1

Hi OCaml community,
Coming from Haskell and about to write a uni project using Frama-C, so I’m currently doing Advent of Code in OCaml to get more comfortable, here’s a quirk I came upon

.ml file:

type 'a my_type = 'a -> unit

let foo (_ : 'a) = ()
let bar = Fun.id foo

.mli file:

type 'a my_type = 'a -> unit

val foo : 'a my_type
val bar : 'a my_type

λ> dune b 
File "lib/ocaml_bug.ml", line 1:   
Error: The implementation lib/ocaml_bug.ml
       does not match the interface lib/ocaml_bug.ml: 
       Values do not match:
         val bar : '_weak1 -> unit
       is not included in
         val bar : 'a my_type
       The type '_weak1 -> unit is not compatible with the type
         'a my_type = 'a -> unit
       Type '_weak1 is not compatible with type 'a
       File "lib/ocaml_bug.mli", line 4, characters 0-20:
         Expected declaration
       File "lib/ocaml_bug.ml", line 4, characters 4-7: Actual declaration

I’ve tried many variations of implementing foo and bar and it only seems like specifying an actual argument for bar resolves the issue. Why is this?

2

You’re hitting the value restriction, check the manual’s chapter on weak polymorphism.

For short, the compiler assumes that the return value of Fun.id foo could hide mutation effects, which would make the more general type unsound, so it uses a weaker kind of type variables that can’t generalize. This looks a bit funny for obviously pure functions, but that can’t be tracked without complicating the type system.

Adding a parameter for bar fixes this because that turns it back into a function definition, which visibly delays the call to Fun.id foo and thus can’t leak polymorphic values across calls. In other words, knowing you come from Haskell: eta-expansion delays side effects.

4 Likes