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,…
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…
Note that OCaml has monadic `do` too, in the form of `let*` operators (and applicative `and`) since OCaml 4.08.
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…
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 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…
> 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…
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…
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…
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…
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…
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…
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,…
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…
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…
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…
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.…
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…
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…
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…
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…
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…
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,…
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…
Note that OCaml has monadic `do` too, in the form of `let*` operators (and applicative `and`) since OCaml 4.08.
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…
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 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…
> 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…
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…
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…
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…
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…
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…
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,…
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…
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…
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…
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.…
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…
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…
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…
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…
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…