Animating type inferences

Stream: new members

[Eduardo Ochs]

Hi all!

I have lots of homemade tools for making underbrace diagrams like this one,

[Eduardo Ochs]

typeinference1.jpg

[Eduardo Ochs]

and even animating them - the image above is the first frame of this animated gif and the first page of this PDF with one frame per page...

[Eduardo Ochs]

...but I've never learned the algorithm for type inference - in the animation above the order of the steps and the names of the types are both improvised.

I searched the internets for other animations of type inferences some time ago and I couldn't find anything.

Anyone knows where I can find an example of a type inference that is "almost animated", in the sense of a text with a diagram and instructions for imagining each frame?

[Eduardo Ochs]

Or: is anyone here interested in helping me to draw one? Here is the core part of the .tex:

[Eduardo Ochs]

sshot.png

[Eduardo Ochs]

The first frame is generated by the 2D ascii diagram in the %L bigstr = [=[ ... ]=] in brown at the top, and the changes between frames are specified in the part in blue...

[Eduardo Ochs]

(Hand-drawn diagrams welcome, of course!)