Eduardo Rafael
@eduardorfs.com
26yo anti floating point developer. You can almost always find me at http://twitch.tv/eduardorfs, it's the boring side of tech.
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...
I'm currently working on deriving all the indexed inductive types and a fully predicative setting.
gist.github.com/EduardoRFS/8...
nat_by_j.v
GitHub Gist: instantly share code, notes, and snippets.
gist.github.com
November 19, 2025 at 5:55 AM
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...
I'm currently working on deriving all the indexed inductive types and a fully predicative setting.
gist.github.com/EduardoRFS/8...
Reposted by Eduardo Rafael
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)
surprise:
FUN OCaml 2026 CFP is open at cfp.fun-ocaml.com/fun-ocaml-20...!
We don't have date yet, nor a venue.
But if you want to speak at FUN OCaml 2026, you can already send us your proposals.
We are contacting venues located in the European Union. If you need a visa, apply early!
FUN OCaml 2026 CFP is open at cfp.fun-ocaml.com/fun-ocaml-20...!
We don't have date yet, nor a venue.
But if you want to speak at FUN OCaml 2026, you can already send us your proposals.
We are contacting venues located in the European Union. If you need a visa, apply early!
FUN OCaml 2026
Schedule, talks and talk submissions for FUN OCaml 2026
cfp.fun-ocaml.com
November 19, 2025 at 4:36 AM
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)
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...
The following, should not have any reentrancy problem and be reasonably fast for some classes of programs.
gist.github.com/EduardoRFS/6...
naive_vars.ml
GitHub Gist: instantly share code, notes, and snippets.
gist.github.com
October 1, 2025 at 10:07 PM
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...
The following, should not have any reentrancy problem and be reasonably fast for some classes of programs.
gist.github.com/EduardoRFS/6...
Reposted by Eduardo Rafael
when you don't know whether you're creating problems for your future self, or solving them
September 23, 2025 at 6:44 PM
when you don't know whether you're creating problems for your future self, or solving them
My technique for mutual recursion works but it currently breaks subject reduction, I need to clean the meta theory a bit.
September 20, 2025 at 6:41 PM
My technique for mutual recursion works but it currently breaks subject reduction, I need to clean the meta theory a bit.
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.
If you know something that I should apply for let me know.
September 17, 2025 at 3:01 PM
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.
If you know something that I should apply for let me know.
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.
September 11, 2025 at 8:55 PM
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.
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.
September 9, 2025 at 1:42 PM
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.
Reposted by Eduardo Rafael
“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!
you’re not supposed to be close to the machine! that’s where the finger munchers are!
September 7, 2025 at 9:39 PM
“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!
you’re not supposed to be close to the machine! that’s where the finger munchers are!
Reposted by Eduardo Rafael
its so stupid that when you are sick you have a hard time to sleep and arent much hungry despite the fact that having both is crucial for good recovery
September 8, 2025 at 9:24 AM
its so stupid that when you are sick you have a hard time to sleep and arent much hungry despite the fact that having both is crucial for good recovery
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.
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.
Thinking on getting HCG with my doctor, but maybe I should just bite the bullet and inject T.
September 6, 2025 at 10:12 PM
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.
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.
Thinking on getting HCG with my doctor, but maybe I should just bite the bullet and inject T.
September 6, 2025 at 10:10 PM
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.
Thinking on getting HCG with my doctor, but maybe I should just bite the bullet and inject T.
I'm thinking on tools to reason about optimizations and as always, code is king. This is a nice way of thinking about it.
September 6, 2025 at 7:51 PM
I'm thinking on tools to reason about optimizations and as always, code is king. This is a nice way of thinking about it.
Reposted by Eduardo Rafael
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.
Give it ~9 months for the inevitable security vuln that this will impact for thousands of desktop users.
September 4, 2025 at 5:12 PM
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.
Give it ~9 months for the inevitable security vuln that this will impact for thousands of desktop users.
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.
It doesn't matter if it is for psychological, psychiatric reasons or performance enhancing, doctors should be allowed to help and warn you.
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.
Half of the reason why I consider something like this is to look more masculine.
Thinking on getting double jaw surgery.
September 3, 2025 at 6:15 PM
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.
It doesn't matter if it is for psychological, psychiatric reasons or performance enhancing, doctors should be allowed to help and warn you.
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.
Half of the reason why I consider something like this is to look more masculine.
Thinking on getting double jaw surgery.
September 3, 2025 at 6:12 PM
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.
Half of the reason why I consider something like this is to look more masculine.
Thinking on getting double jaw surgery.
September 3, 2025 at 6:10 PM
Thinking on getting double jaw surgery.
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.
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.
September 3, 2025 at 5:19 PM
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.
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.
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.
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.
September 3, 2025 at 5:15 PM
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.
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.
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.
Mostly, the underlying calculus has two levels of sharing, a graph based one and an environment based one.
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...
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...
simple-optimal.ml
GitHub Gist: instantly share code, notes, and snippets.
gist.github.com
September 3, 2025 at 5:12 PM
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.
Mostly, the underlying calculus has two levels of sharing, a graph based one and an environment based one.
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...
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...
Reasoning about data using code
YouTube video by Eduardo Rafael
www.youtube.com
September 3, 2025 at 5:08 PM
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...
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...
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...
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...
simple-optimal.ml
GitHub Gist: instantly share code, notes, and snippets.
gist.github.com
September 3, 2025 at 5:05 PM
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...
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...
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...
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...
pi-sigma-self.md
GitHub Gist: instantly share code, notes, and snippets.
gist.github.com
September 3, 2025 at 5:02 PM
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...
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...
