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.