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 performance 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 it can compete, so you should likely take it. 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 will make the RTX 4090 results 10x faster, but keep always in mind, a RTX 4090 still uses at least 100 times more power than a single M3 core at any instant and that in principle GPUs are better for purely parallel tasks.

Also keep in mind that this is a very friendly code to parallelism, this is both against Bend and in favour of it, most real code is not pur

EduardoRFS

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

EduardoRFS

# setup dbus
if test -z "$DBUS_SESSION_BUS_ADDRESS"; then
	eval $(dbus-launch --exit-with-session --sh-syntax)
fi
systemctl --user import-environment DISPLAY XAUTHORITY

if command -v dbus-update-activation-environment >/dev/null 2>&1; then
        dbus-update-activation-environment DISPLAY XAUTHORITY
fi

EduardoRFS

%{
open Tree
(*
type expr = Tree.expr =
  | Literal of int
  | Add of (expr * expr)
  | Sub of (expr * expr)
  | Mul of (expr * expr)
  | Div of (expr * expr)
*)

EduardoRFS

[@@@ocaml.warning "-37-32"]

module Name = struct
  type name = string
  type t = name

  module Map = Map.Make (String)
end

module Var : sig

EduardoRFS

Set Universe Polymorphism.

Set Primitive Projections.
Record ssig (A : Type) (P : A -> SProp) : Type := { l : A; r : P l }.

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.

Definition I_Bool (c_b : C_Bool) : SProp :=

EduardoRFS

```rust
// rules
// Those rules are fully church-style
Γ, x : A |- B : Type
---------------------------
Γ |- @self(x : A). B : Type

Γ, x : A |- M : B[x := @fix(x : A). M]  Γ |- A ≂ @self(x : A). B
----------------------------------------------------------------
Γ |- @fix(x : A). M : @self(x : A). B

EduardoRFS

let Closed A = ∀(G : Grade). A [G]
// closed as it is unknown how many copies it will be needed(0..1)
let Bool : Type = ∀(A : Type). Closed A -> Closed A -> Closed A
let true : Closed Bool =
  // safe to ignore y as it is used 0 times
  ΛG. [ΛA. fun x y -> let [y] = y 0 in x]
let false : Closed Bool =
  ΛG. [ΛA. fun x y -> let [y] = x 0 in y]

// same applies to nats but (0..n)

EduardoRFS

data Bool =
  Bool (exists {n : Nat} . exists {m : Nat} .
    (forall {a : Type} . a [n] -> a [m] -> a))

true : Bool
true = 
  let true_ex_m = 
    pack <0, (/\(a : Type) -> \([x] : a [1]) -> \([y] : a [0]) -> x)>
      as exists {m : Nat} .
        (forall {a : Type} . a [1] -> a [m] -> a) in