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

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

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

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

This is a nice intrinsically typed version of intersection types. I was really looking for something like this to study it in the presence of proof and computationally relevant types.

100

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

A different way of constructing a dependent type theory, we start with an OCaml-like unification theory. To make it second order you just add support for rank-n poly.

120

Eduardo Rafael @eduardorfs.com · 28/12/2024

My current formation for self types requires internal expansion of fixpoints, but there is a class of problems using only eta that is decidable and still provides with the desirable properties. I've been slowly building confident that this is compatible with HoTT but it's easy to make mistakes.

000

Eduardo Rafael @eduardorfs.com · 28/12/2024

Self types must be on the right side of a fixpoint, it may be under a lambda or pair tho, so what happens when you try to initialize and destruct a fixpoint on the same pattern with a self? Well, it actually, works and is not really a special case.

000

Eduardo Rafael @eduardorfs.com · 26/12/2024

Two things, I do streams on twitch daily, mostly working on my own programming language called Teika. And, it's that time of the year where bro's should be mustache maxxing, so let's fucking goo. Link below.

270

Eduardo Rafael @eduardorfs.com · 26/12/2024

Because I have dynamically sized unboxed types, I can have unboxed closures.

000

Eduardo Rafael @eduardorfs.com · 25/12/2024

Sharing a currently old idea, but because I have an unboxed kind, I don't need tuples anymore, unit + pairs is enough. This is a simple trick, but this unlock recursive unboxed types and it is one of the most important ideas that I had this year.

020

Eduardo Rafael @eduardorfs.com · 21/12/2024

I'm liking the Scala syntax for call-by-name.

010

Eduardo Rafael @eduardorfs.com · 20/12/2024

This is actually an interesting feature, it doesn't allow pattern matching as there is no tag, but it's nice to be able to extract things from types naturally.

010

Eduardo Rafael @eduardorfs.com · 19/12/2024

A cool feature of only having types through patterns is that the self type can be implicit.

120

Eduardo Rafael @eduardorfs.com · 19/12/2024

Ascriptions before patterns and expressions is better but none of you are ready for this.

000

Eduardo Rafael @eduardorfs.com · 19/12/2024

This is a real problem in the presence of higher-order unification and let aliases. Interesting enough, storing the original type is very important for error messages.

000

Eduardo Rafael @eduardorfs.com · 19/12/2024

Another idea that I forgot to share, an integration between the formatter and the typer. Whenever you see a type clash, add the typer for the user such that it is easier to find what is the type of each stuff. Of course, this requires good heuristics, people will want to disable it.

210

Eduardo Rafael @eduardorfs.com · 18/12/2024

There is one place where Teika evaluates right-to-left and I will never tell anyone, but, it is almost always a pure expression and if it's not a pure expression it gives you a warning(error by default). This debug will print "hello world". I think it would be possible to make it left-to-right tho.

120

Eduardo Rafael @eduardorfs.com · 18/12/2024

My tip to make very fast compilers, make a bytecode that can be traversed both ways, strong evaluation will produce the bytecode like in a Quine, the equality function will run the bytecode in reverse.

000

Eduardo Rafael @eduardorfs.com · 18/12/2024

Hmm you should be able to extract the commutativity of lets in a CPS setting from parametricity.

000

Eduardo Rafael @eduardorfs.com · 18/12/2024

Yup, types are in my blood.

000

Eduardo Rafael @eduardorfs.com · 17/12/2024

This is pretty cool to see. Notice that the values in p could be unboxed in both cases. I still need to think about some things like optimistic allocation for my unboxed universes, but I'm proud of it.

030

Eduardo Rafael @eduardorfs.com · 16/12/2024

This one is also enough for induction and it's cuter, I think the main idea is that any truncation over equality behavior should be enough for induction.

000

Eduardo Rafael @eduardorfs.com · 16/12/2024

Can you have a consistent theory where this is not true?

000

Eduardo Rafael @eduardorfs.com · 13/12/2024

Yup, this is a major improvement skolem are all explicit and you don't need to have actual lambdas, just functions and closures.

210

Eduardo Rafael @eduardorfs.com · 13/12/2024

A major advantage of my model of type checking is that things like are very intuitive. In fact, it seems like you can extract all of the type checks from functions to below them, this allows you to do type checking after closure conversion or lambda lifting.

100

Eduardo Rafael @eduardorfs.com · 12/12/2024

If you have linearity you can decompose forward references in something cute. This also seems to help understanding why the universe needs to be coinductive, because Forward(K : Kind) is a valid type.

000

Eduardo Rafael @eduardorfs.com · 11/12/2024

This is one of the the things that bothers people a lot. It's trivial by looking at the code that the effect will never happen. And while you could for sure enhance the type with the dependent relationship this sucks. The best tool here is latent types.

000

Eduardo Rafael @eduardorfs.com · 07/12/2024

This could lead to something very close to a single-pass compiler. The LR parsing state machine for this language, matches quite closely with the terms ready for typing and evaluation. This is not an accident, if you have an Strong CBV, this is actually the order that code would also be evaluated.

100

Eduardo Rafael @eduardorfs.com · 07/12/2024

Now that I have a general technique for avoiding accidental duplication during "constraint" generation, many rules look super okay. I write it like the left side, but the final result is the right side.

110

Eduardo Rafael @eduardorfs.com · 06/12/2024

A major issue is that the traditional apply rule breaks sharing, you can see that N is duplicated, from the term level to the type level. The latter on the otherhand preserves sharing, this is an important insight on how to make fast dependently typed systems.

100

Eduardo Rafael @eduardorfs.com · 06/12/2024

I'm having a shit ton of progress and this is half the reason.

030

Eduardo Rafael @eduardorfs.com · 06/12/2024

Beta on an ANF-like, it's messy but it kind of makes sense, all the lets are added right before the caller binder and the caller gets the return. It seems like preserving nested-lets, makes it a better model tho. As evaluation makes a temporary set of lets in the stack.

010

Eduardo Rafael @eduardorfs.com · 06/12/2024

This can be a nice optimization for the typer itself, together with some profit analysis, I can type check the things outside of the dependency graph in parallel. Note that Teika run's it's own code during type checking, so I don't need to do Teika in Teika to benefit.

030

Eduardo Rafael @eduardorfs.com · 05/12/2024

This looks bad, but if you think about it, there is nothing fundamentally bad. To check a forall you need something that infers into a forall, but if it inferred the forall, then the forall is valid, aka you don't need to check it again.

030

Eduardo Rafael @eduardorfs.com · 05/12/2024

Some nice details, in the patter of a function or type function, the internal type is the most internal one, but the one checked against is the most external one.

020

Eduardo Rafael @eduardorfs.com · 04/12/2024

Something like this, of course you can imagine that there are typing rules for the operations themselves. But the simple idea is that you can delay all of your type check as usual, but without invoking another language. This fits super well if you already have monads due to effects.

040

Eduardo Rafael @eduardorfs.com · 04/12/2024

Right, induction-recursion is enough for universes. It also allows to have your types for a typed implementation. Note that there are alternatives(many), just that this seems very principled.

010

Eduardo Rafael @eduardorfs.com · 04/12/2024

Any good reason for this to not be definable?

000

Eduardo Rafael @eduardorfs.com · 04/12/2024

In a dependently typed setting, the following is true.

000

Eduardo Rafael @eduardorfs.com · 04/12/2024

Interesting result, common wisdom tell's us that subtyping such as entering a union leads to information loss. But that's not true in general. In fact, it seems that for most cases there is no true information loss. And yes, here I include Nat <: Int.

120

Eduardo Rafael @eduardorfs.com · 03/12/2024

This is not even my full power.

100

Eduardo Rafael @eduardorfs.com · 03/12/2024

Working on AOC 1, on Teika, the parsing took me some time, I still need to write the sort. Doing things without a stdlib and infix operators is a pain. But it's been interesting. But, I need to connect the typer, doing it without type checking is a massive pain.

181

Eduardo Rafael @eduardorfs.com · 03/12/2024

There is also a true suffix.

100