> I can count on the finger of my hands the number of times when I needed to write explicit types in Ocaml

Do you genuinely rely on whole-program type inference? Writing fewer than ten explicit types in your whole career writing OCaml really surprises me. For example even the OCaml standard library is not written this way.

I find in practice most people explicitly type their top-level functions as if you don't this it can cause type errors at the point of use to 'poison' the function types and cause very confusing errors far away in the program. Do you not see this when you program without any explicit types?

We can see this in other projects for example Crystal which had to back-track on their goal of whole program inference, because it just doesn't really seem tractable in practice.

Why not let the computer do the work? My programming flow in Ocaml has always been:

(1) Hack until I've got something stable. Note: at the start of coding I typically don't quite know what the right abstractions are, so a lot of code (and associated types) are in constant flux.

(2) Once program is stable, wrap it in a module, let the compiler work out all types and put them in as module interface.

That gives me the best of all possible worlds: type annotations at abstraction boundaries but you don't have to type them out. Writing out explicit types inhibits fast change. I wish the languages I'm using at the moment (Scala, Rust, C++) allowed a flow like that. Alas, full type inference stops being possible with more expressive typing systems.

> Why not let the computer do the work?

Because a program's types can serve as part of its documentation.

The other benefit of top-level/function annotations is that they ensure that your mental model of the code is consistent with what the code actually does.

So many times I will accidentally return 42 or Result<Result<42>> when I mean to return Result<42>. With annotations, my error is instantly obvious. Otherwise I accidentally have a function that returns Result<Result<number>> and it may lead to a very weird error message when I use `foo().map(_ + 100)` somewhere else.

That's letting the computer doing more work, not less of it. Relying too much on inference can bow back into the human doing more of the work to figure out what the types actually are in a given spot.

Sometimes an IDE hover can be the best of both worlds - the information is there when you want it (and guaranteed to be accurate since it's using the language compiler's own type inference), but not taking up space when you don't want it.

That helps, but it's orthogonal to adding type annotations.

The computer can only tell you what types your code _has_ (from inference), but not what type it _should_ have based on your intentions. Type inference can only complain when your code contradicts with itself (on a type level), but can't tell you when it contradicts with your intentions.

If you don't write out your intentions, you'd have to hover over everything to see if the inferred types differ from your expectations.

IDE hover types and collapsible type annotations (and alternatively also collapsible implementation) are still useful as a way to declutter your UI when reading code.

This is under-appreciated, and as I have aged I have discovered that I prefer the verbosity over brevity. Namely, when mentoring more junior engineers who can barely write code at all.

It doesn't always make sense to plan the types ahead of time; letting the compiler do the work while you code and then creating a nice interface after is a reasonable way to work.

> let the compiler work out all types and put them in as module interface ... type annotations at abstraction boundaries

Right - that's not global type inference. It's intra-module type-inference.

I don't understand this objection. OCaml does full program inference. I just prefer to wrap things into modules from time to time. That's a pragmatic choice I make, not a restriction on type-inference.

Aside, when I decide to change where I put module boundaries, full program inference helps too: I just throw away the old module definitions, draw different boundaries and re-run inference.

I'm not objecting to anything. This is how I thought most people used inference in OCaml.

You do need to write the types for records though.

Is there anything specific that you find Rust is missing in this regard?

I think Rust deliberately limits type inference to information available in a single function?

Yes.

> Do you genuinely rely on whole-program type inference?

I think their point is that they there were vanishingly few times where they were required to write explicit type annotations. As they say, mostly when dealing with data serialization. That doesn't say whether they wrote more, however.

Except that would then not count the many times where they 'weren't' required to write explicit type annotations solely because they had already written those annotations. Which is not necessarily a unreasonable distinction to make[0], but I can say the same even about C: there have been less than ten times that I got a compiler error because I declared a function or variable without specifying a type for it.

0: There are plenty of places where not supplying a type annotation is more trouble than just writing it. Eg (Haskell since I'm not familiar with OCaml offhand):

  data Foo = FooBar Int String
           | FooBaz [Int]

I'm not even sure how to avoid writing explicit type annotations for Int, String, and [Int] there; maybe OCaml makes it easy, but I doubt I'd bother literally all but less than ten times.

> I'm not even sure how to avoid writing explicit type annotations for Int, String, and [Int] there; maybe OCaml makes it easy

It does make it easy. OCaml has a full matrix of types:

- Nominal product types (records)

- Nominal sum types (variants)

- Structural product types (objects)

- Structural sum types (polymorphic variants)

You could actually always use structural types and never have to actually define types. But OCaml people actually really like the nominal types because their typing rules are stricter and easier for people to understand. But the structural types can come in really handy, e.g. they give you a very convenient way to encode data between libraries that don't need to know about each other. E.g. there is an effort to add JSON-structured output to the OCaml compiler itself. This is using a polymorphic variant type to represent the JSON data type, to avoid having a dependency on any particular JSON library, but still being compatible with popular OCaml JSON libraries ( https://ocaml-community.github.io/yojson/yojson/Yojson/index... ).

That's a type definition. You can't get away without writing out that definition.

If you wanted to, you could use

    Either (Int, String) [Int]

in your code and rely on type inference to do all the work.

> You can't get away without writing out that definition.

Not in Haskell as far as I know, but (assuming MonomorphismRestriction) there's no technical reason why

  data Qwe = Q a
  qwe_eps :: Qwe
  qwe_eps = Q ""

couldn't infer a ~ String in the type definition for Qwe. It's just annoying and pointless, because you never actually care about having to write a explicit type annotation there. (Which was my point.) But it's still a explicit type annotation that you're required to write. (Which was (kind of) chrisseaton's point.)

I guess the idea is:

data Foo a b c = FooBar a b | FooBaz c

or

data Foo a b = FooBar a b | FooBaz [a]

But I agree that writing explicit type annotations is overall better practice.

That declares 'Foo' with kind * -> * -> * -> * , ie a generic type. Whereas I was declaring with kind * , a specific type that might have infered components. Compare:

  quux :: a -> a
  quux x = x
  # quux takes any type genericly
  
  frob y = y () ++ [()]
  # frob takes some specific type, but we don't need to specify which (spoiler alert: it's () -> [()])

Edit: actually the type is generic (not polymorphic) as well.

Why does the kind matter? Both of your examples use type inference and polymorphism - the type 'a' is inferred when quux is used, the type for the second example is inferred from the polymorphic types of (++) and `$`, and both allow to code more freely while in flux.

How much simpler would OCaml or Standard ML be if there were no type inference? I'm perfectly happy to never use type inference (maybe only for local variables).

It feels like people get distracted by H-M inference and forget that there's a pretty nice high level language in SML or OCaml anyway (although I'd rather have modular implicits).

Am I wrong in thinking implementation would be much simpler without type inference?

I think it depends on the algorithm & implementation, but in at least some cases type inference adds very little code over type checking. (To some degree, both are propagating and unifying types through the program and throwing an error when trying to unify two things that aren't the same. And depending on the language, you've got to have some non-trivial machinery for handling function overloads, which can require inference-y reasoning anyway (like calling an overloaded function immediately with the result of another overloaded function).)

On the other hand, non-local inference can make things more complicated in some situations, depending on how hard you try. For instance, Rust gives up if you don't know the type of a variable and you try to accesses a member of it, where I once wrote a more complicated iterative solver that would see if it could infer the type of the variable from later context and return to the member access later. For example, consider the following Rust code where the compiler could figure out the types with some additional complexity but doesn't bother:

  fn main() {
      let a = (1..10).collect();
      println!("{:?}", a.len());
      let b: Vec<i32> = a;
  }

  error[E0282]: type annotations needed

> To some degree, both are propagating and unifying types through the program and throwing an error when trying to unify two things that aren't the same

In fact they're so similar that they can be combined to give 'bidirectional typing'. This is mostly useful for systems that are more expressive than Hindley Milner. For example, dependently-typed languages like Agda and Idris require type annotations for top-level definitions (local definitions can sometimes be inferred). Bidirectional typing is a neater approach to such hit-or-miss inference approaches, and also allows values to be inferred (your function-overloading example is a case of value inference: using the types to figure out which particular function to call).

>Rust gives up if you don't know the type of a variable and you try to accesses a member of it, where I once wrote a more complicated iterative solver that would see if it could infer the type of the variable from later context

My guess is that Rust's designers would reply that their compiler is slow enough without the complication you describe.

Your comment has me feeling quite bullish on TypeScript type inference

HM is pretty easy implement actually. You just need a unification function, the rest is just a laundry list of rules available everywhere, like Wikipedia. Source: I implemented a typed python dialect as a college project that used HM.

> How much simpler would OCaml or Standard ML be if there were no type inference? I'm perfectly happy to never use type inference (maybe only for local variables).

Just the opposite: type inference forces the type systems to remain simpler. Without type inference you could make them more complicated.

Implementation would be simpler, but only by a small degree. To be honest, HM is relatively straightforward to actually implement.

There's some really cool programming language theory that makes things like type inference easier than you think. It's still hard but there's rules and math and stuff for all of it.

You can't actually have a statically-typed language without type inference. Otherwise if you tell the compiler `(5 + 2) : String`, how would it report a type error?

That’s not type inference, just type propagation - tons simpler.

Sorry but what's the difference? Inference is a way to infer the type of any given expression. How does type propagation contrast?

Propagation is way easier, and basically just requires tracking types of values & parameters. To infer the type of `a` in

    var a = 1;

I just need to figure out the type of `1`, then realize that the type of `a` is the same.

slightly harder would be typing union / intersection types - e.g. this:

    var a = some_test() ? "foo" : new Bar();

Java would "infer" (kind-of) the type of `a` to be something like `Serializable & Comparable<? extends Serializable & Comparable<...>>` as both `Serializable` and `Comparable` are supertypes of both `String` and `Bar` (well, depends on `Bar` of course). This starts to show how much trickier things can get.

Now, imagine knowing nothing about what can be stored in the variable, and only seeing how it's used - this is the case for function parameters.

    (x) -> x + 1;

Is `x` a `float`? An `int`? A `long`? Maybe a vector? Basically, imagine the most complex type you can write in a given language, and then consider, the compiler would need to be able to prove that this is the only (or at least the most specific) type you could use.

Hmm, all of your examples can be inferred by Hindley-Milner. Of course, for the second one it would be a type error assuming that `Bar` is not a subtype of `String`. I'm not seeing how type propagation of a complex expression could be any simpler or easier than full-fledged type inference of that expression. For example,

    let x = "foo" |> bar |> baz 5

What's the type of `x`? You might say that we can figure it out by propagation, but how's that different from inference?

Indeed, what I'm saying is that inference is more powerful (i.e. better) than propagation. Most compilers only implement propagation, not full inference, allowing programmers to skip type annotations on local variables (since their types can be propagated from parameters and expressions), but not on parameters.

Basically, there's two complications with type inference. One is type variables that you need to then "solve" - in my last example above, the type of parameter `x` would start as a type parameter α (usually denoted by Greek letters in type systems literature), then it would be "unified" with `int` when used "like" an int (i.e. passed to a function `+ : (int, int) -> int`).

This is what happens in a language with a "simple" type system like OCaml, with no subtyping. (OCaml is slightly more complicated, but still all equations that it needs to solve only involve equality (I think)). If your type system features subtyping, things get a bit more complidated.

    (x) -> new List(x + 1, concat("test", x))

This now generates two constraints, `α <: int` and `α <: string`, that the compiler needs to solve. One solution would be an intersection type `string & int`. Does this type make sense? Does it even exist? Will the programmer understand it? The question isn't only finding the solution, but also which solution is "the best" - how to even define "the best"? I'm not aware of any good answers to this question (not even MLSub, it only works for simple cases).

The other big issue type inference deals with, is generalization. If, at the end of inferring an expression's type, there are no equations involving a type variable (a bit of a simplification, but let's go with it), then it can be "generalized" - turned into polymorphic type.

    (x) -> new List(x)

We might be able to assign the type `forall α . α -> list[α]` (or, a this would be written in Java / C++, `<T> T -> List<T>`), but again this depends on multiple conditions (is `x` used elsewhere? does it escape the scope? is `List` mutable?), and can get much more complicated with more features (e.g. upper and lower bounds, like Java's `<U extends Number>`)

In your example, figuring the type of `x` is trivial compared to above - just take the return type of `baz`.

Local variables seems to be the sweet-spot for me, especially when I'm working on a project with others.

Yes, the main reason to give type annotations is to make debugging easier and as documentation.

In eg Haskell, you often write the types first, even though in principle you seldom would have to write the types at all.

In Rust, I'll usually add a type hint for clarity if I have a massive method chain full of confusing transformations. Sometimes I'll also temporarily add them to closure arguments so that autocomplete is happier.

But otherwise you're right... they're almost never actually needed unless there's an actual ambiguity (e.g. what kind of collection should .collect() produce?)

It's pretty great. I can confidently do a whole pile of reckless-looking stuff and be reasonably confident that I've done what I intended to do once the compiler is happy.

I do this on scala. Given scalac is much slower than ocaml compiler and inference is not as stellar. Regardless, explicit type annotations make code so much easier to read. Anonymous lambdas being an important exception

The real footgun in Scala, to my mind, is implicits.

They are inferred, and that's the point of their ergonomics, but when they are inferred incorrectly, it becomes pretty confusing and sometimes cryptic.

Not to make excuses for the poor errors in the default language, but the "splain" plugin can help a lot, as can ctrl-shift-P in IntelliJ.

The HM type inference used by OCaml breaks down when you add in nominal subtyping, which is common in mainstream static languages like Java. OCaml handles this by giving up subtyping; there is none in the core language, and the (rarely-used) object system uses a form of structural subtyping based on row types.

OCaml also has a really good subtyping implementation in the often-used polymorphic variant system. I'll just quote from http://roscidus.com/blog/blog/2014/02/13/ocaml-what-you-gain... :

> Their real purpose is to support subsets and supersets, which are useful all over the place.

And indeed they are super useful, e.g. I am using them to implement functions that deal with web responses: some can deal with only HTTP responses, some with only WebSocket responses, and some with either. All completely type-safe and extensible.

I once wondered about subtyping[1] too. Looks like there's a possible solution - MLsub[2][3]. But it will require significant amount of work to modify OCaml inference engine to work that way. For now I just use functors for types with the shared fields. It doesn't add too much lines of code either.

[1] https://discuss.ocaml.org/t/function-argument-polymorphism/3...

[2] https://www.cl.cam.ac.uk/~sd601/papers/mlsub-preprint.pdf

[3] https://github.com/stedolan/mlsub

While the object system is pretty rarely used [1], polymorphic variants see quite a bit of use and are also based on row types.

[1] Recently have been seeing a lot more use in BuckleScript because of the JS object representation

Just curious, how would one handle something like this in Ocaml:

  x = function() { 
        if (rand() > 0.5) {
          return "abc"
        } else {
          return 2.01
        }
      }

So far, union types and boxing/unboxing are possible answers. Would type inference work in this case? (well, it would for boxing/unboxing but union types?)

In Standard ML, it would be a type error to do that specifically:

    - if true then "abc" else 2.01;
    stdIn:1.2-1.30 Error: types of if branches do not agree [tycon mismatch]
      then branch: string
      else branch: real
      in expression:
        if true then "abc" else 2.01

You would need to define a new data type to wrap them:

    - datatype string_or_real = r of real | s of string;
    - if true then s "abc" else r 2.01;
    val it = s "abc" : string_or_real

Type error. your lambda doesn't have a valid static type signature. You would wrap that around a union type:

wtf = A of string | B of float

And then you'd return A("abc") or B(2.01) and your function would be () -> wtf

Why's it a type error rather than inferring a sum type?

You can get it to infer the sum type by giving tags to your values with backticks, like `A 1.23 and `B "foo". This will be inferred as "`A of int | `B of string" without you having to declare any type. Without those tags, the system assumes you have made a mistake in returning values of separate types. If it didn't do that, you would not get type errors in many/most (all?) of the situations where you want the type system to help by indicating the inconsistency to you.

Giving tags seems like declaring a type though?

It's not though. If we think about Result as an example, `1`, `Success(1)` and `Failure(1)` are different values, not just different types.

I think the point you're making is that Standard ML has certain restrictions in its type system that are necessary to make type inference possible: there are no union types, no subtypes (more recent work has found a way to make subtyping compatible with full H-M), polymorphism has to be introduced explicitly with `let`, and there are no higher-kinded types. And in some cases you'd argue those restrictions might incur more code overhead compared to a language that loosens those restrictions at the cost of less reliable type inference (e.g. Scala).

That's sort-of-but-not-really true: in my experience union types and subtypes are always bad ideas and there are better alternatives for any use case where you would use them. You never actually want "String | Int", you want a type with meaningful semantics (like `Result<String, Int>`).

If you use the "polymorphic variants" feature with backticks it automatically infers the union. However, most of the time the regular non-polymorphic variants are easier to work with.

A good discussion of this can be found in https://dev.realworldocaml.org/variants.html#scrollNav-4

because "ssdf" is a string but B("asd") is user-defined sum type.

So in the original example, you can't unify "ssdf" and the int 33, but in the re-written version B("sfd") and A(33) have the same type and can be unified.

You might like the language Crystal, it works this way.

https://crystal-lang.org/

But Crystal recently had to walk back from global type inference as they found it was not realistic in practice, didn't they?

Why is it not realistic? Is it too slow or too unreadable?

You could dig up the mailing list messages at the time, but yeah it was slow and I think it produced error messages that were extremely hard to use - it would decide the type of functions was something nonsensical and then report that as an error at all the call sites instead.

Makes sense, bad errors is also why I don't use type inference in my code.

Don't take my word for it but I don't think you can implicitly unify[0] two base type in HM.

https://www.cs.cornell.edu/courses/cs3110/2011sp/Lectures/le...

You cannot unify a string and an integer. 'Base type' is just an abstraction over the enumerable primitive types (bool, unit, char, etc). It's generally understood that these are simple cases to unify, so they aren't even mentioned most of the time.

If you are interested for a language that does something like that then check out https://archive.is/Op8Mf or the other words by Stephen Dolan

In haskell you would do it like

    import System.Random
    x = do y <- randomIO :: IO Float -- note: this is before there are instances of randomIO for IO Int and other types
           if y > 0.5 then
             return (Left "abc")
           else
             return (Right 2.01)

I think another interesting question is, how would you handle the return value of such function in your code?

You would have to either:

- test for the type of that value in order to handle it properly,

- rely of the implicit cast rules of JS, which wouldn't be very useful here I suppose

As it has been said by others, in Ocaml (as well as in many other strongly typed languages) you can use a sum type to solve that problem.

Edit: In some languages, there is also the concept of "intersection types" which, if I understand correctly, let one also handle that sort of situation. The corresponding Wikipedia entry [1] gives a list of languages supporting that concept, and provides examples.

[1]: https://en.wikipedia.org/wiki/Intersection_type

I've found this type of function useful for duck typing, and I've generally found duck typing to be a really useful tool to add polymorphism to code.

The point I was trying to make is that if you have to rely on runtime type information, you might as well use sum types in a more strongly typed language, where the scope of the code gets limited to the type itself.

With "duck typing", you need to have an extra test for types which your code is not supposed to work with, whereas with sum types, the type checker will help you verify that it cannot happen.

That being said, there are situations which a strong type system will not be able to model.

Anyway, at the end of the day, what matters is that you (and your coworkers) feel comfortable with your code. I know by experience that it's not always the case.

I find unions without a tag hard to handle.

To expand on another commenters example, suppose you have a sum type that models successful computation with a return value or a failure with an error message.

If you have tags / constructors, that's all easy. But if you just use naked unions, you can not write code that deals with error messages (or strings in general) in the success case.

I can’t speak for Ocaml, but in Elm, an if expression as well as a function must return the same type. Therefore the code you posted would be invalid.

To expand slightly, the Elm compiler will help you out here and show you what you need to fix. Given this function body

  randomReturner n =
      if n < 0.5 then
          123
      else
          "abc"

The compiler will give you the following info:

  The 2nd branch of this `if` does not match all the previous branches:

  22|     if n < 0.5 then
  23|         123
  24|     else
  25|         "abc"
            ^^^^^
  The 2nd branch is a string of type:

      String

  But all the previous branches result in:

      number

  Hint: All branches in an `if` must produce the same type of values. This way, no
  matter which branch we take, the result is always a consistent shape. Read
  <https://elm-lang.org/0.19.1/custom-types> to learn how to “mix” types.

  Hint: Try using String.toInt to convert it to an integer?

You can try it out on Ellie here: https://ellie-app.com/9nXxfKSStG4a1

In TypeScript, x would be of type () => "abc" | number.

Wouldn't it be string|number unless using the `as const` modifier?

It used to be. But more recent versions of TypeScript (I believe since 3.5) are much stricter with strings in implicit unions. It's really quite helpful.

Here's an example where the feature can save you:

```

let x = () => {

    if (Math.random() > 0.5) {

        return "abc"

    } else {

        return 4

    }

}

// ERROR: This condition will always return 'false' since the types '"abc" | 4' and '"sdf"' have no overlap.

if (x() === "sdf") {

   do_work()

}

```

In F# (which is very similar to OCaml), you’d have to explicitly cast the return value to “obj” to get this to compile.

Just to clarify to people not familiar with the two languages and their differences, this is somewhere where the two languages diverge greatly. OCaml does not have an "obj" type that we can cast to (and in general casts are quite rare).

You would need to declare that the function returned a sum type (string | int).

> I could not understand why most static language required writing so many types that were easy to deduce and why people where saying that not having to write types made dynamic language better.

In Scala, a lot of libraries end up with deduction-only types—ie, types that can only be deduced, because actually typing out the type signature is very long, complicated, and filled with generics-upon-generics. I don’t find that to be a pleasant outcome—if I can’t fill in the type signature myself, trying to understand what the code is going to do ends up that much more complicated. Yet that’s not an uncommon situation.

But why the complexity? Most libraries should have "simple" types.

They mostly do. The cases where you get complex types is where you are using dependent typing. For example, imagine you wanted to write an "update" method. So we have this datatype:

    data Address(line1: String, line2: String, postcode: String)
    data User(name: String, address: Address, phoneNumber: String)

And here's an example of what "update" should do, in JSON:

    // Argument 1
    {
      "name": "Bob",
      "address": {
        "line1": "123 Fake Street",
        "line2": "Beverly Hills",
        "postcode": "90210"
      },
      "phoneNumber": "555-555-5555"
    }
    // Argument 2
    {
      "address": {
        "line1": "377 Fake Street"
      },
      "phoneNumber": "555-555-4444"
    }
    // Result
    {
      "name": "Bob",
      "address": {
        "line1": "377 Fake Street",
        "line2": "Beverly Hills",
        "postcode": "90210"
      },
      "phoneNumber": "555-555-4444"
    }

This kind of function is the kind of thing that keeps people using dynamic languages. It's easy, and obvious, what it should do, and what its type signature is, but in most typed languages you can't write it without constructing a whole parallel hierarchy of datatypes by hand.

Scala is one of about 3 languages where you can actually write this in a nice way and it will be correctly typed. But the type you get will be:

    (User, Field[Label['name], Option[String]] :: Field[Label['address], Option[Field[Label['line1], Option[String]] :: Field[Label['line2], Option[String]] :: Field[Label['postcode], Option[String]] :: HNil]] :: Field[Label['phoneNumber], Option[String]] :: HNil) => User

And until recently it was even worse than that because the compiler didn't know to print the "::" types as infix.

Now with first-class record support in the compiler you could improve this a little bit, but fundamentally there's not really any better way to write that type. Maybe if the language had first-class support for dependent types like Idris you could write ti as `(User, UpdateTo(User)) => User` or something, but the reader would still need a way to find out what `UpdateTo(User)` was concretely. So what do you do?

They should, but when the types are all inferred, it’s easier to hide that complexity.

Interesting that you say that. I come from a very different background but have always that thought type inference hurts the readability of code and should be used sparingly.

I wrote up the thoughts in a post [1] that seemed to get extreme reactions from both camps [2].

[1] Type inference has usability problems. http://web.eecs.utk.edu/~azh/blog/typeinference.html

[2] HN discussion. https://news.ycombinator.com/item?id=20296123

Careful, there are multiple ways to use type inference.

In practice, many people use type inference when exploring and writing code; but then add explicit annotations for readability and documentation. You could even do the last step automatically.

Does the bytecode OCaml compiler compile faster than Go? What about Bucklescript? I've never experienced issues with OCaml compile times but I wonder how it compares against a widely acknowledged "fast" compiler.

I think its safe to say it's fast in the general sense, the first time I compiled Revery I didn't believe that it had actually worked it was so fast. Just tried it again 0.98 secs to compile 20-25k lines of native OCaml/Reason.

I'd be interested if anyone found/ran any benchmarks, though I thinks its pretty hard to write a fair compile time benchmark. I did a quick search and came across this post comparing solving the same problem with haskell/ocaml/go, which just kind of off hand mentions the compile times. OCaml versions range from 0.3-0.8s and Go was reported as ~1s.

https://pl-rants.net/posts/haskell-vs-go-vs-ocaml-vs/

In that case maybe generics aren't a compile time killer. (Although I'm quite curious how the OCaml compiler compiles so quickly).

Go people have a very weird understanding of generics, and that messes up many discussions.

They typically mix up parametric polymorphism and ad-hoc polymorphism.

I blame C++'s templates for the confusion. (And Go people's common refusal to look much further, and especially not into academia..)

> And Go people's common refusal to look much further, and especially not into academia..

I don't think that's a fair statement, given Phil Wadler's formal work on generics in Go - "Featherweight Go" (https://arxiv.org/abs/2005.11710) - which is acknowledged here: https://blog.golang.org/generics-next-step

Yes, hence my weasel word with 'common' and 'most'.

It's good to see that they are taking the likes of Phil Wadler serious. (Perhaps his beard helps?)

> We’d like to thank Philip Wadler and his collaborators for thinking formally about generics in Go and helping us clarify the theoretical aspects of the design.

In the older post at https://blog.golang.org/why-generics you still see them pretty much mix up parametric polymorphism and ad-hoc polymorphism.

Thanks for the link to the paper!

Technically OCaml typechecking is exponential in the length of your program, but really that's just because it's exponential in the depth of your most deeply nested `let` construct, and most people don't actually write programs that look like

    let a = ...
      in let b = ...
        in let c = ...
          in let d = ...

Wait, that's actually really common in OCaml though. I mean not the indentation of course, but every series of let-bindings is essentially a single nested expression. That's just the way let-bindings work.

Generics in the sense of C++ templates can be a compile time killer. However generics in the sense of HM type systems are basically just asking the compiler to fill in the type for you, which it has already figured out. HM type inference in general is ~O(n) (and exponential in the worst case, but you basically have to try to do that)

Right, so there are two reasons that C++ templates hurt compile times:

1. C++ templates don't require you to treat the type variables as opaque; depending on what the body of a template does with its type parameters it may or may not type check depending on how the variable is instantiated. By contrast, in OCaml (and most languages) generic functions cannot assume anything about their type parameter. This means that the compiler can type check the body of the generic function once and be done, rather than having to essentially check it at every call site.

2. Aside from type checking, C++ templates generate separate code for each instantiation of the type parameters. This (generally) results in faster code as it is specialized to the type in question, but it means more code is generated, which of course takes time (and it can also bloat the executables). This is probably a bigger deal than the type checking part. By contrast, OCaml only generates one copy of the code for a function, which simply doesn't care about the types of its arguments. This is also a common implementation strategy; Java does something similar.

Note that Rust also suffers from (2), but not (1).

You can get OCaml to behave like 2, but you need eg Generalised Algebraic Datatypes or some magic with modules to do so.

See https://blog.janestreet.com/why-gadts-matter-for-performance... and https://blog.janestreet.com/more-expressive-gadt-encodings-v... for why you'd sometimes want the behaviour in 2.

(I do agree, that that behaviour is a bad default.)

Yeah I wonder what the actual cost is of (2). I know the Standard ML compiler MLton takes the monomorphization (2) approach as well, with good success. I'm currently writing a toy SML compiler for fun, and I'm planning on doing the same, since you get better run time performance, assuming you're using that info to do unboxing.

There is ongoing discussion [1][2][3] to enable more aggressive optimization for "Flambda" switches, in some cases this can bring more than 2x times speedup.

[1] https://github.com/ocaml/opam-repository/pull/16753

[2] https://discuss.ocaml.org/t/ocaml-4-11-first-beta-release/60...

[3] https://discuss.ocaml.org/t/ann-bap-2-1-0-release/5906/9

Note that code that relies on inference too much is really hard to read without an IDE. So reading it e.g. in the github web interface is a really bad experience.

It's because Hindley-Milner doesn't play well with subtyping.

You do get subtyping in Ocaml with modules and "module types", but in that case you are explicitly spelling out the module types. They're not inferred.

Note that there's some more recent research that bridges the HM-subtyping gap:

http://stedolan.net/research/mlsub.pdf

So this can be done, though afaik there's still some theory work to be done to combine it with some of the more advanced features in modern FP languages (e.g. higher rank types)

> my single use case for explicit types in Ocaml was data deserialization

Data deserialization is where types are most useful