The post "A Very General Method of Computing Shortest Paths" (https://r6.ca/blog/20110808T035622Z.html) shows that the Gauss-Jordan algorithm for solving matrix equations, the Floyd-Warshall algorithm for all-pairs shortest paths, and Kleene's algorithm for converting DFAs to regular expressions, are all the same algorithm on matrices of elements from a star-semiring.
I do think adding a Noita-style cellular automaton would be fairly straightforward.
Currently Veloren has water and lava, but neither will flow (e.g. if water blocks are manually placed on top of a hill, they won't flow downhill, fortunately this is rare due to worldgen). A simple way to fix this would be to have an ECS system that uses CA-style rules (e.g. a water block with an adjacent-and-below air block swaps places with that air block), though naively doing this would be expensive (iterating over all loaded terrain chunks every tick). A possible optimization would be to detect such blocks, remove them from the main terrain grid, put them in a separate entity-with-terrain-collider (the same kind we use for airships), and only iterate the (sparsely populated) AABB of fluids-that-have-recently-moved. This is similar to what Noita does with keeping track of recently-updated terrain rectangles. Once this is in place, it can be straightforwardly extended with more fluid interactions (e.g. Minecraft-style water + lava = obsidian, more Noita-inspired gases rising).
The contrast between Gauss-Jordan[0] and the Bareiss algorithm[1] is a good example of explicitly handling the length of the numbers in bits as part of the runtime.
Gauss-Jordan is O(n^3) if you consider addition and multiplication to be constant-time, but if it operates on arbitrary-precision integers, it can get exponentially slow[2].
The Bareiss algorithm avoids this worst-case behavior by choosing the pivots in a slightly more involved manner, which avoids building up large intermediate values.
Section 5.13 advises building a custom type-and-mode checkers (per project, seemingly).
Section 4.1 defines a specific type-and-mode system in enough detail that it seems machine-checkable (potentially with the declarations as-is, with suitable declarations of unary `+` and `-` via `op/3` for modes).
It feels like an omission that the paper doesn't recommend or even mention the existence of an implementation-agnostic, project-agnostic type-and-mode checker.
Has one been developed since the paper was published, or is this not as useful as it would seem/not done for some other reason?
There are a few community libraries, for example see the Swi-Prolog packages typedef [1] and typecheck [2] (the latter implementing Hindley-Milner). Unfortunately there isn't anything like an accepted standard (although the package typedef is very popular).
My experience is that type- and mode-checking in Prolog programs tends to be ad-hoc and simplistic, for example it's common to test whether an argument is ground or not and therefore enforce a certain mode (or sets of modes):
% p(+X,-Y)
%
p(X,Y):-
ground(X)
,var(Y)
,...
For slightly more complex type-checking the Prolog ISO standard provides predicates like integer/1, atom/1, atomic/1 etc [1]. These don't make up a proper type system but they can go a long way towards catching common errors.
A subtler point is that Prolog programs tend to use unification to perform type-checking by pattern matching an argument to a (Prolog) term. For example (borrowed from a Prolog course I'm GTA'ing):
This will fail for any (at least partially ground) input to max_heap/1 that doesn't match the term h(K-V,L,R), here used to represent a binary heap, or the atom "epsilon", for the empty heap. The representation of a heap in this way is entirely up to the programmer but Prolog's built-in unification will essentially provide type-checking for free when a complex data structure like this is used.
If your source language has some construct that you want to express as state machines (e.g. async, CPS, pattern match compilation), and you want to compile the state machine as direct threaded code[0] (which involves fewer branches than a while-switch), then if you're compiling to C, you need computed gotos[1], which are non-standard.
It's definitely the case that some of the ELF header fields can be repurposed to store additional data, the following articles all address that optimization:
There are also a few instructions in the article that are size-suboptimal (e.g. "movl $4, %eax" is 5 bytes (b804000000), while the equivalent "xor %eax, %eax; movb $4, %al" is only 4 bytes (31c0b004)).
I tried to do it as optimal as possible, but I think there is indeed more to be saved with putting code in the elf header, i'm not very familiar with the elf format. This is as small as I could get it without doing that, just using yasm, ld and strip.
The relevant file of source code has, "Copyright (c) The University of Glasgow 2001", which jibes with my memory of having used Dynamic in GHC in 2004 or earlier:
Also notice that Dynamic is in the Haskell Package Repository's "base" package, described as containing "Basic libraries", not part of an ancillary area for user-contributed libraries:
There exist type systems of which great grandparent is an accurate description (the most well-known of which is probably that used by Typescript) but the type system of, e.g., Haskell, Ocaml or Rust is not it.
(Now I am getting curious what specific programming language's type system great grandparent had in mind.)
Which is an entirely different package, and the relevant types are entirely different. Only the name is the same. The `dynamic` package does indeed appear to be an april fools joke.
The Dynamic type in base is about runtime reflection, which is occasionally useful but not something that comes up often and not really about rapid prototyping.
>The Dynamic type in base is about runtime reflection, which is occasionally useful but not something that comes up often
It is not something that comes up often, but since I am used to languages like Javascript or Scheme, when it does come up, figuring out how to do it in Haskell, e.g., satisfying the monomorphic restriction, has occasionally diverted my focus away from the problem to be solved for hours while I learn more about Haskell's type system.
But yeah, what I just wrote is in no way inconsistent with the comment I initially replied to, namely,
For a concrete example of how z3 differs from Coq, consider trying to prove that "for all integers x, there exists an integer y greater than x such that x divides y" (a subgoal of Euclid's theorem on there being infinitely many primes).
Here's a transcript of using the z3 python bindings to ask for a proof:
$ python
>>> import z3
>>> x, y = z3.Ints('x y')
>>> s = z3.Solver()
>>> s.add(z3.Not(z3.ForAll([x], z3.Exists([y], z3.And(y >= x, y % x == 0)))))
>>> s.check()
unknown
z3 returns unknown (if it had returned "unsat", it would have been possible to extract a resolution-refutation proof), and there's not much that can be done with the unknown.
Here's a Coq interactive session that proves most of the cases (with one subproof left unsolved, it was taking me too long relative to the rest of the proof).
$ coqtop
Require Import NArith.
Require Import Omega.
Lemma x_le_fact : forall x, x <= fact x.
induction x;.
- simpl; omega.
- simpl; admit. (* Proving `x <= fact x -> S x <= fact x + x * fact x` left unsolved here *)
Admitted.
Goal forall (x : nat), exists (y : nat), y >= x /\ Nat.modulo y x = 0.
intros x; exists (fact x).
split.
- unfold ">=". apply x_le_fact.
- induction x.
+ simpl; reflexivity.
+
(* goal here is `fact (S x) mod S x = 0` *)
unfold fact; fold fact.
(* goal here is `(S x * fact x) mod S x = 0` *)
rewrite (Nat.mul_comm (S x) (fact x)).
(* goal here is `(fact x * S x) mod S x = 0` *)
apply (Nat.mod_mul (fact x) (S x)).
discriminate.
Qed.
Unlike z3, you need to manually tell Coq what the steps are, but it gives you feedback on which steps are correct, and what assumptions are available and what subgoals still remain at each step (I've included some of those as comments, running the proof through the interpreter shows more detail).
