octachron

Not really when reading `iter (printf %"d %d" m) ns`, I am likely to read it in three steps

  - `iter`: this is a side-effect on a collection
  - `(printf`: ok, this is just printing, I don't care about what is printed, let's skip to the `)`
  - ns: ok, this is the collection being printed

Notice that having a lambda or a partial application `_` will only add noise here.

> But to a reader it is valuable information whether it's partial or full application.

This can be a valuable information in some context, but in a functional language, functions are values. Thus a "partial application" (in term of closure construction) might be better read as a full application because the main type of concern in the current context is a functional type.

The issue is that the C memory model allows more behaviours than the memory model of x86-64 processors. You can thus write code which is incorrect according to the C language specification but will happen to work on x86-64 processors. Moving to arm64 (with its weaker memory model than x86-64) will then reveal the latent bug in your program.

Note that OCaml has monadic `do` too, in the form of `let*` operators (and applicative `and`) since OCaml 4.08.

OCaml has structural variants in the form of polymorphic variants. On the product side, OCaml has objects, first-class modules, labelled tuples (since OCaml 5.4) which are all a form of structural records, with different trade-off in term of ergonomics.

For a bounded size of types of sub-expressions, HM inference is quasi-linear in the size of the program, because the constraints appearing in the HM algorithm are only equality between meta-variables.A NP-complete SAT solver is not really a good fit for this kind of simple constraints. Even more so when typechecking often represents a significant part of compilation time.

(Of course the tricky part of the definition above is that the size of types can theoretically be exponential in the size of a program, but that doesn't happen for programs with human-understandable types)

Nearly the same as with positional argument: Partially applying a function to a named argument creates a closure with this argument filled in, and you can apply the argument in whichever order you want:

    let f a ~x ~y b = a + x + y + b
    let g = f ~y:1 (* g is closure with the argument named ~y filled in *)
    let h = g 2 (* another closure with the first positional argument filled in *)
    let int_15 = h 8 ~x:4 (* = g 2 8 ~y:4 = f ~y:1 2 8 ~x:4 *)

The more complex interaction is rather with type inference and currying, or the interaction between currying and optional arguments.

A point that I find missing in the timeline for dynamic array is that there have been implementation for dynamic arrays available in libraries for more than twenty years.

However, none of the authors of those libraries were really happy with their own implementation because those implementations had to choose between performance, API usability or thread safety.

When I closed the student pull request (which was a naive implementation with no unsafe features), it was with the idea that it was unfair to expect a beginner use to solve those issues.

The subsequent iterations explored different part of the design space before the final iteration which converged to safely using unsafe language features to reach a new local API optimum.

> This introduction doesn't really explain anything, as I guess it assumes you've learned OCaml elsewhere and are just here to practice.

Indeed the link is a not an introduction to OCaml but a demo instance of Learn-ocaml which is framework for building online exercise websites to complement (online or physical) lectures. This is why the instance is hosted on the OCaml Software Foundation website rather than ocaml.org: the demo is not targeted to learners but to teachers.

You are misreading the quantification, a value l of type List a means that for all type a, the element of the list has type a. In other words, this is an universal quantification whereas your interpretation is an existential quantification.

This is obviously only possible if the list itself has no elements, and indeed a simple proof is that the statement above is valid for the empty type: all elements of a list of type List a have type empty (among other types). Thus there are no elements in this list.

And both Haskell or OCaml can prove it:

     type empty = | (* this is defining a never type *)
     type polymorphic_list = { l: 'a. 'a list } 
     (* OCaml require to explicit construct polymorphic type *)

     let polymorphic_lists_are_empty ({l} : polymorphic_list ) =
     match (l:empty list) with
     | [] -> () (* this is the empty list *)
     | _ -> . 
     (* this clause requires to the OCaml typechecker to prove that the remaining cases are unreachable *)

Return (or other effects) does make sense as an expression in a functional language. Typically, OCaml has `raise Exception` which is also an expression, with the same type as `return` or any never returning function. And exceptions can also be used to implement a user-defined `return` function.

A significant factor in my experience is that a lot of programs are quite similar from an compiler perspective: they use well-trodden set of features and combine then in a predictable way. Compiling those regular programs is well-tested and well-understood. Compiler bugs tend to be relegated on the exotic paths, when using language features in novel and interesting ways.

Note that this is an error message from the ocamldoc tool, and not an error message from the OCaml compiler itself. Funnily enough, looking that the repository history, this French error message was introduced in the very first version of ocamldoc in 2002 and went undetected (or unreported) for 9 years. Thanks for the historical tidbit!

How long ago was this "relatively recently"? When I translated all the remaining French comments in the OCaml compiler nearly 10 years ago, there were already no warnings nor error messages in French.

Mathematicians are more interested in the gap in our proof framework.

Like stated in the articles, many "interesting" constants appearing in mathematics feels like obviously irrational. However, proofs that they are irrational have been eluding mathematicians for centuries.

This contrast is seen as a sign that we may be just missing the right mathematical insights. And if we find this insight, we might be able to adapt it to unlock other open problems in mathematics (or computer science?).

This is one of these cases where the path (the new proof framework) is expected to be much more interesting than the initial destination (the fact that yes the Euler constant is irrational, of course).

This is only true for distributions with finite variance (and the edge case of distribution with slowly growing infinite variance).

And for a given variance, gaussian distributions are exactly the maximal entropy distribution.

The variable "x" would be a list in this case. This the GADT (Generalized Abstract Data Types) syntax, where the type of the whole union can depend on the discriminated union case. Thus

      List_name: 'a list -> ('a, list_name) app

reads: for any value "x" of type "'a list", "List_name x" constructs a value of type "('a, list_name) app". In this case, it is the the "list_name" tag part of the type which is dependent on the union case.

Ocaml object system can also achieve this in a quite lightweight way

    type foo = < foo:int >
    type bar = < bar:int >
    type k = < foo; bar >
    type u = < k; baz:int >
    let f (x: <u; ..>) (\* the type annotation is not needed \*) = x#m

The Everest project did publish a proved TLS implementation: https://mitls.org. And at least the EverCrypt* cryptographic primitives has been used outside of academia.

F* has an extraction backend which targets "human-readable C" code, contrarily to Coq which extracts proof to "machine-written OCaml" (typically the extracted code use a type-system-escape-hatch left in OCaml for the sake of Coq extraction). Consequently, part of the Everest project (the proven cryptographic primitives in particular) has been integrated into C code base like the linux kernel, firefox .

Adding type annotations in OCaml never reduce the typechecking time: it adds more information for the typechecker to process and it can only increase the size of type. Typechecking time is proportional to the size of types but those tends to stay constants and small inside normal project. I think that F# should have a similar behaviour?

Note that OCaml has been using autoconf since OCaml 4.09.

Predictions of the solar system state are accurate only on "short" periods. The solar system is chaotic, and predicting its state after few million years is no more possible that predicting the weather for next year. This does not preclude making very accurate on short period.

Note that n-body problems are not particularly complex or hard to solve compared to other chaotic systems. In many ways, the existence or nonexistence of closed-form solutions is mostly a distraction: it merely reflects our choice of primitive functions and there is no sets of primitive functions that is stable for addition, multiplication, composition, inversion and integration. Typically, even the simple integral ∫ eˣ/x dx cannot be decomposed into more elementary functions.

But that doesn't matter in practice, because we are already using numerical approximation to compute primitive functions that are not implemented in hardware. Using numerical solvers to compute solutions to ODE is not so different. A good illustration of that point is that there is an analytic solution for the 3-body problem (in the form of an infinite series in t^{1/3}). But this solution is useless for computing orbits because it has bad convergence properties. In other words, it is better to use a numerical solver rather than stick to the analytical solution. And a similar phenomenon exists for polynomial equation of degrees 3 and 4: the exact formula is numerically unstable, and its better to use a numerical solver when one wants a numerical solution.

Ok, now I understand: this part is a description of how optimizing C bindings using the OCaml FFI often requires to play around the GC:

With OCaml uniform representation of data, the GC will follow all data that looks like a pointer in its reachable set of values. Which is the right thing to do for valid OCaml values, for which anything that looks like a pointer (outside of strings or numerical arrays) is a pointer to a valid OCaml value.

However if you are building OCaml values in the C FFI, and that this in-construction value is somehow reachable by the GC, you have to make sure that there is no pointer in the uninitialized part of the data. Or alternatively you need to make sure that the runtime will not enter a GC phase while you are building those values.

Of course not.

Honestly, I am not sure what was the initial sentence before being distorted by the editor. The next sentence makes me think that the interviewee might have been discoursing about all the tricks that Janestreet uses to reduce allocation to a minimum but it is hard to tell from the final text.

No, OCaml compiles polymorphic functions once by using an universal representation of values which tends to play better with a type system with recursively polymorphic functions, higher-rank polymorphism or existential types (which all imply that concrete types are not always known statically in OCaml).

For GADTs heavy programs, it depends a lot on how much work the exhaustiveness check for pattern matching is doing behind the scene: With GADTs, one can encode a Turing machine in the type system. In that pathological case, analyzing that a pattern match is exhaustive might require to check if the encoded Turing machine stops in n steps. Consequently, it is perfectly possible to write programs where the compiler spends 99% of its time on analyzing pattern matching. But it is also possible to write GADTs heavy programs that don't require such expensive analyses.

I have no first-hand experience with Swift but the previous discussion at https://news.ycombinator.com/item?id=12108876 and the description of the problematic algorithm seems to indicate that numerical or mathematical code can run quite easily into the issue.

However, I must add that type inference algorithms being exponential in the source code size is nothing new: OCaml and Haskell inference are also exponential in the source code size. But that is because the size of types can be exponential in the source code size. Moreover, type inference complexity in OCaml and Haskell is linear in the size of types. And since in practice, no one ever uses exponentially growing types, type inference stays well behaved.

The specific issue with Swift is really more that even for simple result types, the inference may still have to do an exponential amount of guess work.

Fast (and principled) inference for not-too-complicated polymorphic types is an explicit design goal for OCaml and Haskell languages. And this design goal constraint quite a lot the type system.

Typically, there are many type system features that break this property and where OCaml and Haskell requires type annotations (for instance polymorphic functions that takes polymorphic functions as arguments and use them in a polymorphic way).

As a consequence, typechecking for OCaml programs tend to take from 10% to 60% of the whole compilation time for typical programs. However, for OCaml programs that make heavy use of GADTs typechecking can dominate the compilation time (probably due to the exhaustiveness check but I have yet to empirically check that).

Infamously, Swift made the choice to introduce a typechecking algorithm with an exponential complexity in the size of expression (to support function overloading and literals) even for simple types.

The OCaml object system is still parametric polymorphism (trying to pass itself as subtyping polymorphism through row variables) rather than ad-hoc polymorphism: there are still no functions that only work on a finite subset of types. In other words, a function may work on any objects that has a method `m`, but you cannot have the same method that has different implementation for `int` and `float`.

In this comparison, "purer" more often than not means that the choice simplified the formalization of SML.

And for the context, many people from the OCaml side considers that the SML formalization has been for a good part responsible for the freezing of SML since 1997.

I am not sure how F# which started as a .NET version of early OCaml 3 can be seen as a modernized OCaml 5? Even more so when F# has to give up on some OCaml core feature in the transition (before growing in its own language of course).