Introspection?

[mgubi]

I was interested in learning more about HVM by extending it with some functionalities to make it more amenable to be directly programmed in the style of interacting Lisp systems. I know that HVM is meant to be a compilation target, but it seems also quite interesting as a general programming platform (see recent discussion on HOP by @zicklag, for example). A thing I had in mind was to expose some internals, like the possibility to add rules at runtime or to create new terms programmatically: this would be the equivalent of quote/unquote. The can be a family of constructors which describe a general term or a rule of the language and a function which converts these representations into terms which can then be reduced. For example something like:

(make_term (HVM.Ctr "+" [10,20])) => (+ 10 20)
(parse "(+ 10 20)") =>  (HVM.Ctr "+" [10,20])

Would be also nice to be able to reify terms into representations which can then be manipulated by programs. E.g. write a REPL directly in HVM.

Does it makes sense or I'm overlooking some fundamental problem?

[zicklag]

To my knowledge ( which is incomplete and may be wrong ), I think you could do something along those lines.

I think it'd be possible to experiment with without modifying HVM by using it as a library and writing Rust function implementations for things like make_term.

---

I'm not sure if that should be built-in to HVM, though, or if it should be added to a more specific HVM runtime, maybe something along the lines of #219.

Since, to use HVM as a useful programming environment, we're going to need a collection of good bindings to things like file/network IO, etc., maybe a reflection API ( if you could call it that ), would live in that kind of a project, instead of in the hvm runtime itself.

[mgubi]

I indeed tried along the lines you suggest, e.g. add an external function which convert a string into a nullify constructor, but it seems to me that one needs some cooperation from the runtime. At the moment it is not possible to modify the program that reducers use, nor introduce new symbols, due to restrictions in the Rust types. However, I'm new to Rust, and it is possible that I do not understand very well the current codebase. Constructor names are translated into numbers quite early in the parsing of the file. Actually, it seems possible that different RuleBooks would come up with different ids for the same constructors, this would pose a problem if one calls add_book several times on the same Program to add rules incrementally.

[zicklag]

I succesfully made this work without changes to HVM:

(Message) = "This is my message"

Main = (Test.make_constructor "Message")

And Main will return "This is my message". The caveat is that it must loop through every name in the program and compare it with "Message" to find the "Message" constructor, also I haven't done argument parsing, but that should be completely possible.

We might be able to fix the need to loop through all the names by creating a "name to ID" map in the Program.

Here's the ( very messy ) code:

https://gist.github.com/zicklag/9531beef260f5ee9fdd25be38b81f222

[mgubi]

Nice! I indeed wanted to have a global symbol table. Also I was wondering if reduction of constructors via rules should really be in the core: it seems an optimization which could be done independently of the reduction mechanism. Essentially each reducible constructor is just a symbol bound to a compiled function which pattern match and eventually substitute. This compiled function could be an interpreter for the rules or in a more advanced version of HVM could JIT compile the rule and then pass control to the compiled code. If a new case for the rule is added then it will recompile the rule. In this way on has full control of the reduction mechanism and can also implement "object oriented" construct, where the head of a term is not a constructor but an object and the reduction of the term would be to send a message to the object (e.g. the rest of the term) to determine its reduction. In particular I have in mind the minimalistic structure of Maru (https://piumarta.com/software/maru/). Basing such a system on interaction nets will remove the need to GC and add automatic parallelism / async execution.

[zicklag]

Also I was wondering if reduction of constructors via rules should really be in the core: it seems an optimization which could be done independently of the reduction mechanism.

I was wondering about that, too. I'm really new to interaction nets and most of the architecture of HVM, but it seemed to me like maybe the core reducer should only execute interaction nets or interaction combinators, with an escape hatch of some sort for IO and maybe, like you say, constructors.

I'm not sure, I'm still trying to wrap my head around the consequences of that and get a better grip what the whole architecture looks like currently.

[mgubi]

More generally it would be nice if rules were not "special" but first-class objects. Somehow an evaluation seems more the joining of a term and a context which give meaning to its constructors (and free variables). It seems to me that even DUP nodes are not really floating around but associated to the current evaluation context. One could imagine to be able to reify the context and manipulate it. I wonder if one could bridge the interaction calculus picture with considerations related to the computational interpretation of sequent calculus (see e.g. Wadler, Philip. ‘Call-by-Value Is Dual to Call-by-Name’,)