21–30 of 51 posts
Interesting, though I can’t help but feel that the tone of the first few paragraphs could be a bit more.. humble? Even if the underlying model is much better, you can’t really compare a complete project to one that is alpha. Real world complexities catch up in the later phase of bigger projects. Nonetheless, I eagerly await its future.
Earlier quoted context omitted.
Are you hiring?
Yes, starting next week or so! We'll be looking for engineers that have skills relevant to our projects, including compilers, low-level assembly optimization, functional programming, type theory, parallel computing, and so on. Right now, we're quite busy with incorporation and bureaucracy, but you should see job postings in our to-be-released landing page (higherorderco.com) soon. Meanwhile, I answer DMs on Twitter (…
[1] https://www.semanticscholar.org/search?q=typed%20assembly%20...
namely, Greg Morrisett and Neal Glew's work
https://www.semanticscholar.org/author/J.-G.-Morrisett/14364...
https://www.semanticscholar.org/author/MorrisettGreg/1643921... (semantic scholar incorrectly thinks there are two Greg Morrisetts)
Earlier quoted context omitted.
Hi Victor, it's great to hear your ideas on how to tackle the issue. Do you have an example or a sketch of how strategic lambdas can be used to avoid unnecessary cloning? I'd love to hear more. Indeed, if one were to figure out how to strategically add appropriate mechanisms to share data, perhaps the issue can be solved. It seems a highly nontrivial problem - but perhaps it would have taken someone brave as you to t…
Of course! Let me write a complete overview on the subject. Consider the following program: (Foo a b) = (If a (F b) (G b)) It is easy to note that Foo makes an unnecessary clone of the 'b' variable, since it is used in different branches. This could be avoided by adding a lambda, as follows: (Foo a b) = ((If a λb(F b) λb(G b)) b) That is what I mean when I said that, in most instances, cloning can be avoided by addin…
The case of erasing nodes after duplication 'unnecessarily' must be handled and cannot be dismissed - being much of the core use case of lazy evaluation.
From your breakdown it suggests that compilers to HVM use some heuristic which uses `&` immutable references on most data-like nodes, and lazy duplication on code-like nodes. I'm quite sure that still doesn't solve the issue of unnecessary duplications in the general case, but it does seem plausible that such measures suffice to slice the Gordian Knot in practice, similar to how you eliminated the 'oracle' with your superposition resolution - to very practically sidestep the uncommon, complicated case. Indeed, the distinction between code-like nodes and data-like nodes dictates very much of their behaviour during reduction, whereas in much of PLT literature and pure interaction nets, every node is 'code-like'.
I'm not sure if this is good enough in practice, if as I believe, HVM is meant to be a compiler target; I fear that good heuristics may not be enough, where the 'unnecessary' erase-after-duplicates arise from complex code paths, and may perhaps become apparent intermittently (but catastrophically) or only be clear on inspecting compilation output.
Looking forward to more of your work!
One thing that I don't see addressed (and the main problem I had with Haskell) is the predictibility of runtime: if I change a function somewhere to be 2x slower by doing something differently can it have a much bigger than 2x difference in functions that use it? With Rust, the type system guarantees safety and predictable runtime as well. I don't see how any model that doesn't have linear / affine typesystem impleme…
https://github.com/HigherOrderCO/HVM/issues/167
I discuss how HVM is able to perform deforesting, one of the core techniques that made GHC so fast, "for free" at runtime, without being explicitly hardcoded. That is great, but the point I'd like to make is how I show that: by measuring the 'rewrite count' of a program with HVM's '-c' flag. It shows you how many rewrites a program evaluation took. Since each rewrite is a constant time operation, this gives us a very precise metric of the complexity of a program.
On the issue above, I implemented two versions of the same function, and measured their rewrite counts. Here are the tables:
Fn V1
N | rewrites
- | --------
0 | 402
1 | 802
2 | 1202
3 | 1602
4 | 2002
5 | 2402
6 | 2802
7 | 3202
8 | 3602
9 | 4002
Fn V2
N | rewrites
- | --------
0 | 1403
1 | 1408
2 | 1413
3 | 1418
4 | 1423
5 | 1428
6 | 1433
7 | 1438
8 | 1443
9 | 1448
TimeComplexity(FnV1(N)) = 402 + 400*N rewrites
TimeComplexity(FnV2(N)) = 1403 + 5*N rewrites
Earlier quoted context omitted.
Of course! Let me write a complete overview on the subject. Consider the following program: (Foo a b) = (If a (F b) (G b)) It is easy to note that Foo makes an unnecessary clone of the 'b' variable, since it is used in different branches. This could be avoided by adding a lambda, as follows: (Foo a b) = ((If a λb(F b) λb(G b)) b) That is what I mean when I said that, in most instances, cloning can be avoided by addin…
Thanks for the detailed breakdown of your analysis! The case of erasing nodes after duplication 'unnecessarily' must be handled and cannot be dismissed - being much of the core use case of lazy evaluation. From your breakdown it suggests that compilers to HVM use some heuristic which uses `&` immutable references on most data-like nodes, and lazy duplication on code-like nodes. I'm quite sure that still doesn't solve…
https://wiki.xxiivv.com/site/interaction_nets.html
If someone is looking for a graphical playground to experiment with interaction nets, here's Sylvain Lippi's InTwo(gtk):
https://github.com/max22-/intwo
Anyone looking to better understand linear logic in the context of IN ought to have a look at Victor's Absal:
https://github.com/VictorTaelin/abstract-algorithm
Someone below linked to Baker's excellent linear lisp paper(psi-lisp), I'd like to augment this recommendation with Linear Completeness theory of combinators:
One thing that I don't see addressed (and the main problem I had with Haskell) is the predictibility of runtime: if I change a function somewhere to be 2x slower by doing something differently can it have a much bigger than 2x difference in functions that use it? With Rust, the type system guarantees safety and predictable runtime as well. I don't see how any model that doesn't have linear / affine typesystem impleme…
Predictability is one of the most exciting aspects of HVM, to me. That's because everything is linear, so time and space costs are completely measurable, in a way that resembles C, but even more profoundly. For example, in the following GitHub issue: https://github.com/HigherOrderCO/HVM/issues/167 I discuss how HVM is able to perform deforesting, one of the core techniques that made GHC so fast, "for free" at runtime…
https://reader.elsevier.com/reader/sd/pii/S0890540197926432
It's funny, that as a BTC maxi I'm not fond of new tokens (like Cardano) being created, but the work they are funding are exceptional (my favourite is Vitalik funding a lot of longevity science, which would be the job of the governments, but they don't do anything about it).
Some more questions:
- Are you planning GPU backends? (emitting parallel C code and using CUDA / OpenCL compilers, like how Tinygrad does
- Can the code be used as a more efficient Jax / PyTorch compiler in the future? AI code is functional, though the building blocks (basic instructions, register, cache sizes, memory bandwidth) are the main optimization criteria
Earlier quoted context omitted.
Predictability is one of the most exciting aspects of HVM, to me. That's because everything is linear, so time and space costs are completely measurable, in a way that resembles C, but even more profoundly. For example, in the following GitHub issue: https://github.com/HigherOrderCO/HVM/issues/167 I discuss how HVM is able to perform deforesting, one of the core techniques that made GHC so fast, "for free" at runtime…
I wish I could say that I understand you, but at least what you write is exciting enough for me to read the paper that you linked, as it looks simple enough even for me: https://reader.elsevier.com/reader/sd/pii/S0890540197926432 It's funny, that as a BTC maxi I'm not fond of new tokens (like Cardano) being created, but the work they are funding are exceptional (my favourite is Vitalik funding a lot of longevity scie…
To address your questions:
Yes, we have plans for GPU backends. In fact, I have even written a working prototype some time ago! It reduces λ-terms on the GPU using the same rules as HVM, with all the locks and atomics in place, and it seems to achieve a near ideal speedup, even with thousands of nVidia cores:
https://gist.github.com/VictorTaelin/e924d92119eab8b1f57719a...
That said, it is still just a single-file prototype. Sadly, we couldn't include a GPU backend on this funding round, but it is definitely something we'll be investing in a future, specially if we manage to grow as a company. Imagine writing pure Haskell functions and they run in thousands of GPU cores with no efforts? Pure functional shaders, physics engines...
Regarding PyTorch, I don't think HVM would be more efficient than it for ML, because PyTorch is already maximally optimized to use GPUs to their limit. HVM should be seen as a way to run high level programs in a massively parallel fashion without needing to write low level CUDA code yourself, but it won't outperform manually optimized CUDA on GPUs. That said, I do believe interaction net based processors would greatly outperform GPUs by breaking the Von Neumann bottleneck and unifying memory and computation in billions of nano-interaction-cores. I do believe such architecture could one day empower AI and make our LLMs and RNNs much faster.
This reminds me strongly of Absal[0]. Could somebody familiar with both give a comparison? This looks like a really cool idea, and I'd love to see a GHC backend for it. It might also be nice to have a brief explanation if an interaction between without just linking to a big theory paper. [0] https://github.com/VictorTaelin/abstract-algorithm eta: I only now notice that Victor Taelin is the author of both packages.