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

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

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 · 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 · 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

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 · 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 · 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

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

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 · 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

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

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

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

Thinking on getting double jaw surgery.

010

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

Status Report 5: Very WIP, my understanding of induction / dependent elimination is starting to lead to novel result. The following allows you to derive induction, this is the first result that I have that when done correctly doesn't necessarily implies an irrelevant equality.

010

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

Status Report 4: I finally figured out how to properly implement univalence, the nice thing is that when combined with self types, you get all of HoTT. Yes, I'm aiming quite a bit high here, but the pieces are slowly fitting together. The proofs are underway, maybe I can do ICFP 2027.

010

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

You should probably not use it as an interpreter or compiler, maybe for a theorem prover, but my tip, understanding why this works gives a new set of tools for sharing(think fast compilers). Mostly, the underlying calculus has two levels of sharing, a graph based one and an environment based one.

020

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

Status Report 3: I recorded a video about using high-level languages to reason about performance. I didn't like the approach, I was reading a screenplay and it felt weird, but the content is quite useful. www.youtube.com/watch?v=pxTr...

youtube.com

Reasoning about data using code

YouTube video by Eduardo Rafael

020

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

Status Report 2: I was able to derive a new family of techniques for optimal reduction. Mostly splitting sharing from renaming by context capturing substitutions. There is an NbE implementation and an abstract machine is underway, but will take some time. gist.github.com/EduardoRFS/f...

gist.github.com

simple-optimal.ml

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

020

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

Status Report 1: In the last months I finished the development of my dependent type theory with self types, it should have decidable checking and subject reduction. The strong normalization proofs are still underway, but I'm aiming to prove it for all PTS. gist.github.com/EduardoRFS/1...

gist.github.com

pi-sigma-self.md

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

040

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

I'm back here, giving it another try, as Twitter keeps being a shithole.

3280

Reposted by Eduardo Rafael

Hank Green @hankgreen.bsky.social · 17/05/2025

Since we’re in a relatively safe space…this post is terrible messaging and I am baffled that it gets likes. Its root message is “who cares about the truth, just do the stuff /I/ think is right!!”

2303112151

Eduardo Rafael @eduardorfs.com · 16/05/2025

Deriving induction using self types and pairs has a couple advantages. gist.github.com/EduardoRFS/a...

gist.github.com

self_types_with_sigma.md

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

120

Reposted by Eduardo Rafael

NPR @npr.org · 15/05/2025

For the first time, doctors have created a customized treatment using the revolutionary gene-editing technique known as CRISPR to treat a baby with a rare, life-threatening genetic disorder.

npr.org

A promising genetic treatment tailor-made for a baby born with a rare disorder

For the first time, doctors have created a customized treatment using the revolutionary gene-editing technique known as CRISPR to treat a baby with a rare, life-threatening genetic disorder.

1143261657

Reposted by Eduardo Rafael

metame メタミ @metameeee.bsky.social · 06/05/2025

funny how people that don't come from fp hate giant pattern match expressions... I think it's one of the easiest control flow constructs to follow

6191

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

I need to learn algebraic signatures.

000

Reposted by Eduardo Rafael

Adolfo Neto @adolfoneto.elixiremfoco.com · 16/04/2025

If you go to @cbsoft.bsky.social, you can have this view every morning

591

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

I didn't fully grasp why this happens, but it reminds me of the positive but not strictly positive recursion + impredicativity. okmij.org/ftp/Haskell/...

okmij.org

Impredicativity Bites

Demonstrating Russell paradox arising from the combination of impredicativity, the case analysis on types and some sort of injectivity of type constructors.

010

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

Thinking about internalizing parametricity.

000

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

I'm still looking for a self verifying rewriting system.

000

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

Just go and disable smooth scrolling. It's just better.

010

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

This feels like a general technique for decomposing self down. Here I'm relying on internal expansion of fixpoint but it's truly not needed. If my intuition is right, I should publish this.

020

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

I think this one is well typed. A proof of induction for the booleans extracted, using sigma + identity + mutual recursion. I'm not sure if it leads to self, as it may not be general enough, but I'm still working on it. Note, this is compatible with HoTT.

020

Reposted by Eduardo Rafael

sai @texoport.in · 26/02/2025

just a little bit of diet coke in a regular sized “glass”

251

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

I was playing with an optimizer and noticed that substitutions from the variables to the binders could be nice and as always there is a paper. www.ccs.neu.edu/home/shivers...

ccs.neu.edu

020