11 ms·

Ocaml use Hindley-Milner type inference. I was taught programming with it and ended up deeply spoiled. I could not understand why most static language required

• dwohnitmok 6y ago
  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.
  • dropofwill 6y ago
    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/ https://pl-rants.net/posts/haskell-vs-go-vs-ocaml-vs/
    • dwohnitmok 6y ago
      In that case maybe generics aren't a compile time killer. (Although I'm quite curious how the OCaml compiler compiles so quickly).
      • shpongled 6y ago
        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)
        • zenhack 6y ago
          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).
          • shpongled 6y ago
            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.
          • eru 6y ago
            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/ https://blog.janestreet.com/why-gadts-matter-for-performance... and https://blog.janestreet.com/more-expressive-gadt-encodings-via-first-class-modules/ 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.)
  • xvilka 6y ago
    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 https://github.com/ocaml/opam-repository/pull/16753 [2] https://discuss.ocaml.org/t/ocaml-4-11-first-beta-release/6042 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 https://discuss.ocaml.org/t/ann-bap-2-1-0-release/5906/9
• wenc 6y ago
  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?)
  • deleted 6y ago
    [deleted]
  • jldugger 6y ago
    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
    • chrisseaton 6y ago
      Why's it a type error rather than inferring a sum type?
      • iaabtpbtpnn 6y ago
        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.
        • chrisseaton 6y ago
          Giving tags seems like declaring a type though?
          • 6y ago
• ohazi 6y ago
  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.
  • AzzieElbab 6y ago
    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
    • nine_k 6y ago
      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.
      • lmm 6y ago
        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.
• chrisseaton 6y ago
  > 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.
  • eatonphil 6y ago
    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?
    • shpongled 6y ago
      Implementation would be simpler, but only by a small degree. To be honest, HM is relatively straightforward to actually implement.
    • miloignis 6y ago
      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
• azhenley 6y ago
  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 http://web.eecs.utk.edu/~azh/blog/typeinference.html [2] HN discussion. https://news.ycombinator.com/item?id=20296123 https://news.ycombinator.com/item?id=20296123
  • eru 6y ago
    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.
• iaabtpbtpnn 6y ago
  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.
  • ohadrau 6y ago
    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
  • xvilka 6y ago
    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/3224/2 https://discuss.ocaml.org/t/function-argument-polymorphism/3... [2] https://www.cl.cam.ac.uk/~sd601/papers/mlsub-preprint.pdf https://www.cl.cam.ac.uk/~sd601/papers/mlsub-preprint.pdf [3] https://github.com/stedolan/mlsub https://github.com/stedolan/mlsub
  • yawaramin 6y ago
    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/#polymorphic-variants 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.
• mcphage 6y ago
  > 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.
  • The_rationalist 6y ago
    But why the complexity? Most libraries should have "simple" types.
    • mcphage 6y ago
      They should, but when the types are all inferred, it’s easier to hide that complexity.
    • lmm 6y ago
      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?
• literallycancer 6y ago
  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.
  • deleted 6y ago
    [deleted]
• acchow 6y ago
  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.
  • zenhack 6y ago
    Note that there's some more recent research that bridges the HM-subtyping gap: http://stedolan.net/research/mlsub.pdf 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)
• lxe 6y ago
  > my single use case for explicit types in Ocaml was data deserialization Data deserialization is where types are most useful