iiinova — where your digital self keeps evolving

Eduardo Rafael @eduardorfs.com · 01/09/2026

I'm happy with this, it seems like my take on self types naturally converge to some of the work on displayed categories. I MAY HAVE CATEGORIAL SEMANTICS FOR DEPENDENT TYPES.

030

Reposted by Eduardo Rafael

Kiran @kirancodes.me · 08/04/2026

Ran into one of my old college buddies today dude was one of the most cracked devs I knew. like reverse engineer a os from binary cracked found out she transitioned. I asked her why, and this hit me like a ton of bricks, "kiran, a computer contains no techbros, but millions of trans sisters"

16855142

Reposted by Eduardo Rafael

Alice ✨ @welltypedwit.ch · 01/08/2026

is there anyone that actually understands how rice's theorem works omfg rice's theorem does not say that you can't prevent bad things from happening in a turing complete programming language.

2304

Eduardo Rafael @eduardorfs.com · 26/07/2026

@welltypedwit.ch pinging you boss because you know people, also I'm proud of this and it's surprisingly useful.

000

Eduardo Rafael @eduardorfs.com · 26/07/2026

It's been a while, just sharing more victories, I was succeful in coming with up a presentation of self types that has(conjectured) decidable type checking and only Pi Types + Self Types. This is a blog post on it, it gives some nice examples, HITs and CPS of sigma. gist.github.com/EduardoRFS/2...

gist.github.com

self_types_are_great.md

GitHub Gist: instantly share code, notes, and snippets.

110

Eduardo Rafael @eduardorfs.com · 06/01/2026

I dunno man, I cannot stop feeling like we can do better.

110

Eduardo Rafael @eduardorfs.com · 06/01/2026

Seriously, X is just not a great place, but this one feels too artificial, I'm kind of depressed with the state of affairs in general.

260

Reposted by Eduardo Rafael

Alice ✨ @welltypedwit.ch · 02/01/2026

programmers are such babies. you're paid an obscene salary for an extremely comfortable job for ostensibly being smart and good at logical thinking. you can figure out how to run the 4 opam commands required to set up an ocaml project oh my god

6637

Eduardo Rafael @eduardorfs.com · 03/01/2026

Pior que a minha leitura do assunto é mto teórico.

020

Eduardo Rafael @eduardorfs.com · 19/11/2025

It definitely makes it harder to reason about performance tho.

010

Eduardo Rafael @eduardorfs.com · 19/11/2025

I think I forgot to share this here, deriving induction for the inductive types in an impredicative setting, using pairs and equality without UIP only. I'm currently working on deriving all the indexed inductive types and a fully predicative setting. gist.github.com/EduardoRFS/8...

gist.github.com

nat_by_j.v

GitHub Gist: instantly share code, notes, and snippets.

020

Reposted by Eduardo Rafael

sabine 🐫🦀 / "use ocaml"; @sabine.sh · 19/11/2025

folks, if you want FUN OCaml 2026 to happen, please put in some drafts (it's okay if you change your mind later, both regarding topic and whether you can attend)

241

Eduardo Rafael @eduardorfs.com · 06/11/2025

It was not intentional bro.

020

Eduardo Rafael @eduardorfs.com · 06/11/2025

No idea, but T even has acute effects.

120

Eduardo Rafael @eduardorfs.com · 01/10/2025

It's interesting that naive mutable variables work for interpreting the lambda calculus if you're restricting the evaluation order. The following, should not have any reentrancy problem and be reasonably fast for some classes of programs. gist.github.com/EduardoRFS/6...

gist.github.com

naive_vars.ml

GitHub Gist: instantly share code, notes, and snippets.

010

Eduardo Rafael @eduardorfs.com · 28/09/2025

Even if it's a new symbol, it's still cyclical, it really doesn't matter semantics wise, if A is isomorphic to B and B implies in something that includes A, then B is cyclical. Also, it's called a fixpoint, because you go back to the same point.

000

Eduardo Rafael @eduardorfs.com · 26/09/2025

This a cycle, you just showed that it is well founded as it eventually finishes, but the stream type is also a regular tree and there is no trivial way of avoiding the cycle.

100

Eduardo Rafael @eduardorfs.com · 26/09/2025

A list type is a regular tree, it's not a tree as it is cyclical.

100

Reposted by Eduardo Rafael

sabine 🐫🦀 / "use ocaml"; @sabine.sh · 23/09/2025

when you don't know whether you're creating problems for your future self, or solving them

Alt text: A meme featuring two Kermit the Frog characters - the regular Kermit on the left and "Dark Kermit" (Kermit in a dark hood) on the right, with white text at the bottom reading "come to the Obj.magic side". This appears to be a programming humor meme referencing OCaml's Obj.magic function, using the classic "good Kermit vs evil Kermit" meme format to represent the temptation to use unsafe type casting.

071

Eduardo Rafael @eduardorfs.com · 20/09/2025

My technique for mutual recursion works but it currently breaks subject reduction, I need to clean the meta theory a bit.

000

Eduardo Rafael @eduardorfs.com · 20/09/2025

I'm just a con man, I don't even know greek.

020

Eduardo Rafael @eduardorfs.com · 17/09/2025

Hey, I'm open to giving talks(maybe lectures?) about whatever, either in South America, Europe or North America. If you know something that I should apply for let me know.

070

Eduardo Rafael @eduardorfs.com · 17/09/2025

Or it was dune, but something includes it.

010

Eduardo Rafael @eduardorfs.com · 17/09/2025

Either OxOCaml has it or it's an OCaml Pro thing.

220

Eduardo Rafael @eduardorfs.com · 13/09/2025

A vontade de morder crianças é realmente universal.

120

Eduardo Rafael @eduardorfs.com · 11/09/2025

Similarly but simpler than distilling optimality, you can distill Weak CBV from a Strong CBV interpreter + explicit laziness. In such a scenario, you can see that beta + force is equivalent to a single beta in the weak setting.

020

Eduardo Rafael @eduardorfs.com · 09/09/2025

People call it portable assembly for a reason tho. And we definitely say that it is a native language.

010

Eduardo Rafael @eduardorfs.com · 09/09/2025

It's both, in the same way that there is a program in C and the equivalent program in Assembly, those are two different presentations of the same program.

000

Eduardo Rafael @eduardorfs.com · 09/09/2025

You can trivially compile WebAssembly to native.

020

Eduardo Rafael @eduardorfs.com · 09/09/2025

I've been on TRT now, aiming to stay a bit on the high end but still under 1000. Also monitoring my DHT because I don't want to start balding again.

010

Eduardo Rafael @eduardorfs.com · 08/09/2025

The general advantage of teaching X with LLM is to also teach on how to learn some other X. The issue is that you and most people thinking on education want to teach a very specific X.

010

Eduardo Rafael @eduardorfs.com · 08/09/2025

nonsteroidal anti-inflammatory drugs and metamizole

000

Reposted by Eduardo Rafael

horse shoe crab programmer @myrrlyn.net · 07/09/2025

“c gets you close to the machine” is the kind of sentence that lands very differently after working in a factory you’re not supposed to be close to the machine! that’s where the finger munchers are!

1342158

Eduardo Rafael @eduardorfs.com · 08/09/2025

This is the main reason why I started to control mild symptons, like mild fever and mild inflammation issues, mostly because otherwise I will starve myself to death.

000

Eduardo Rafael @eduardorfs.com · 07/09/2025

Also, on testosterone, taking Androgel, but I was trying to keep my testicles working.

000

Eduardo Rafael @eduardorfs.com · 07/09/2025

Clomid doesn't inhibit aromatase, it's a SERM.

000

Eduardo Rafael @eduardorfs.com · 07/09/2025

Clomid and HCG raises testosterone and estradiol.

000

Eduardo Rafael @eduardorfs.com · 06/09/2025

I'm at the point of my life where, I understood that if I keep myself health by doing most things right, I can take performance enhancing substances and still be healthy.

000

Eduardo Rafael @eduardorfs.com · 06/09/2025

Depression, an insane headache, no libido and at times talking was weird.

000

Eduardo Rafael @eduardorfs.com · 06/09/2025

Tried anastrozole + clomid, the estradiol didn't lower that much, but I definitely felt the brain damage from low estradiol in the brain. Thinking on getting HCG with my doctor, but maybe I should just bite the bullet and inject T.

210

Eduardo Rafael @eduardorfs.com · 06/09/2025

A slightly different intuition, Bool and Unit are not isomorphic, they have different amount of elements(cardinality), (Bool -> Unit) has only one element(take whatever and return unit), so Bool -> Unit cannot be isomorphic to Bool.

010

Eduardo Rafael @eduardorfs.com · 06/09/2025

I'm thinking on tools to reason about optimizations and as always, code is king. This is a nice way of thinking about it.

020

Reposted by Eduardo Rafael

John McBride @johncodes.com · 04/09/2025

DHH also made the baffling decision to go ahead and fork Chrome - all just for 2 small patches that change the color theme to match the hyperland theme: github.com/omacom-io/om... Give it ~9 months for the inevitable security vuln that this will impact for thousands of desktop users.

github.com

GitHub - omacom-io/omarchy-chromium

Contribute to omacom-io/omarchy-chromium development by creating an account on GitHub.

5204

Eduardo Rafael @eduardorfs.com · 03/09/2025

Related to this, I also don't think you should need to justify yourself on why you want to do something with your body. It doesn't matter if it is for psychological, psychiatric reasons or performance enhancing, doctors should be allowed to help and warn you.

040

Eduardo Rafael @eduardorfs.com · 03/09/2025

People joke that TRT is gender affirming care for cis men, but I actually think it is true to some people. Half of the reason why I consider something like this is to look more masculine.

020