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.
And “happen to work on x86-64 processors” also will depend on the compiler. If you write
*a = 1;
*b = 'p';
both the compiler and the CPU can freely pick the order in which those two happen (or even execute them in parallel, or do half of one first, then the other, then the other half of the first, but I think those are hypothetical cases)
x86-64 will never do such a swap, but x86-64 compilers might.
If you write
*a = 1;
*b = 2;
, things might be different for the C compiler because a and b can alias. The hardware still is free to change that order, though.
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.
Ages ago working on PS2 games one of our guys had a particularly huge "do-animations-and-interpolations-and-state-and-everything-for-the-hero-in-one-huge-switch" thingy (not uncommon to encounter in games) that crashed the GCC, the function was split up.
In the sequel I think a similar function grew enough that not only had they the function but also split in multiple files to avoid miscompiles.
Most recently I was generating an ORM binding(C#) from the database model of an ERP system, for mysterious reasons the C# runtime was crashing without stacktraces,etc (no debugger help). Having seen things like this before I realized that one of the auto-generated functions was huge so I split it up in multiple units and lo-and-behold it worked.
(Having written a tiny JVM once I also remembered that jump instructions are limited to 64kb, not 100% if the .NET runtime inherited that... once it worked I didn't put any effort into investigating the causes).
Most of the time though compiler bugs aren't the worst (unless they help cause confusion in already hard scenarios).
reply