EduardoRFS

// Post: https://x.com/VictorTaelin/status/1854326873590792276
// Note: The atomics must be kept.
// Note: This will segfault on non-Apple devices due to upfront mallocs.

#include <stdint.h>
#include <stdatomic.h>
#include <stdlib.h>
#include <stdio.h>
#include <time.h>

EduardoRFS

(* follow me on https://twitter.com/TheEduardoRFS *)

module Existentials = struct
  (* packed *)

  type show = Ex_show : { content : 'a; show : 'a -> string } -> show

  let value = Ex_show { content = 1; show = Int.to_string }

  let eval_show ex =

EduardoRFS

Set Universe Polymorphism.
Set Definitional UIP.

Inductive eqP (A : Type) (x : A) : A -> SProp :=
  | eqP_refl : eqP A x x.

Definition C_Bool : Type := forall A, A -> A -> A.
Definition c_true : C_Bool := fun A x y => x.
Definition c_false : C_Bool := fun A x y => y.

EduardoRFS

{-# OPTIONS --guardedness #-}

module stuff where

open import Agda.Builtin.Equality

symm : ∀ {l} {A : Set l} {n m : A} → n ≡ m → m ≡ n
symm refl = refl

record Pack {l} (A : Set l) (fst : A → A) : Set l where

EduardoRFS

type never = |
type ('a, 'b) equal = Refl : ('x, 'x) equal

type ('l, 'r) dec_equal =
  | D_refl : ('l, 'l) dec_equal
  | D_neq : (('l, 'r) equal -> never) -> ('l, 'r) dec_equal

let ( let* ) v f = Option.bind v f

module Nat = struct

EduardoRFS

title	date	tags
Reversing normalization for errors	2024-08-02 13:00:00 -0700	errors rewriting theory

Normalization is a technique used to ensure that any two objects that represent the same thing have the same form aka the normal form, a unique form of an expression.

EduardoRFS

const printOnce = function (data) {
  let printed = false;
  return function () {
    if (!printed) {
      console.log(data.byteLength);
    }
    printed = true;
  };
};
function demo() {

EduardoRFS

module Cube = struct
  type color = R | G | B

  module Face = struct
    type face = {
      mutable s0 : color;
      mutable s1 : color;
      mutable s2 : color;
      mutable s3 : color;
      mutable s4 : color;

EduardoRFS

Bend vs Reality

TLDR: I understand the proposal of Bend, but when the efficiency reduction is so big that a RTX 4090 is only 7x faster on a near-optimal scenario than 2 cores of a M3 Max in a language like JavaScript, you should probably not take it.

On the otherhand, easy to use, but opt-in, parallel languages such as OCaml exists and they can compete, so you should likely take those. If you need even more performance, Rust could likely beat the RTX 4090 results on a mobile CPU.

Of course future optimizations should improve Bend results, but my goal here is to show that the current results are not as impressive as they may look, likely a JIT would make the RTX 4090 results 10x faster, but an RTX 4090 still uses at least 100 times more power than a single M3 core at any instant, additionally in principle GPUs are better for purely parallel tasks.

Also this example is a very parallelism friendly, this is both against Bend and in favour of it, most real code is not pure and not a purely binary alg

EduardoRFS

type User = {
  id: number;
  name: string;
};
type Data = {
  user: User;
  date: Date;
  instance: number;
};