counterexamples
counterexamples copied to clipboard
stedolan
Counterexamples in Type Systems
The cast `(A)x.o` can be removed from this code sample by replacing the `public Object o` field of `Ex` with a `public A o` field. This change produces the following...
The following MetaOCaml code, distilled from > [Generating code with polymorphic let a ballad of value restriction, copying and sharing](https://tohoku.pure.elsevier.com/en/publications/generating-code-with-polymorphic-let-a-ballad-of-value-restrictio) > Oleg Kiselyov involves an unsound interaction between three MetaOCaml...
This PR adds three more examples of monotonicity failures in OCaml, relating to 1. the relaxed value restriction and strict positivity 2. compatibility 3. labeled arguments Another possible addition involves...
Pages like https://counterexamples.org/runtime-misinformation.html apparently adapt to the OS light/dark colour mode: on MacOS in dark mode with Firefox or Chrome, the code snippets are dark text on dark background, and...
First of all, thanks for the great work! http://counterexamples.org/unstable-types.html The counterexample by Russo is due to open-scope unpacking of first-class modules and *applicative* functors. The easiest way to fix the...
Hi, I'm not sure it's in the spirit of the (great) book but I thought you might like https://blog.adacore.com/the-most-obscure-arithmetic-run-time-error-contest Thanks for sharing the book for free!
Both Agda and Idris had unsoundness caused by using IEEE floating point equality as definitional equality, whereby `0.0 == -0.0` despite the two values being different and behaving differently. In...
The section “Eventually, nothing” states: > according to the C standard, compilers are allowed to assume that the program contains no infinite loops without side-effects. This is inaccurate; the precise...
https://counterexamples.org/distinctness-recursion.html Coherence in Rust is used to check that there are no overlapping trait impls. Failing to prevent overlapping impls can be exploited to get memory unsafety. Coherence works by...
