# Proposal: Image

###### tags: `Juvix` `juvix-project`

What Is the Juvix Image System
==============================

The definition for Image can be found in the terminology section. As for
the image system itself, it is the way we are able to talk about Juvix
in Juvix. It allows us primitives in Juvix to be able to reason over
what is in scope, or to change and add to the system while it\'s live.
It is a very powerful technique that allows Juvix to do a lot with
little effort.

## Preamble

When one is evaluating programming and programs, one is often deceived, as the final code that is on the screen is just the result. It tells you nothing of how one derived the code.

Programming is thus an interactive process. Some simply write some code, and then ask the compiler what is wrong with their code if anythings. Others, have a more conversational attitude and talk to the language via the repl or indirectly through tooling. Others may still do more and have the system dump information and fill in parts of the code. These however are never written down, and all trace of this information is lost, only brought up when people talk about the language and their experience with the language's "tooling".

Thus tooling is an important factor for people and what languages they stick with. Though the view of tooling when its talked about is often taken separate from the language itself. After all, we can point to languages with many compilers that have different kinds of deployment and editing tooling. The flaw in that argument is that it assumes the language does not lay the platform from which these systems can exist. Even worse, these systems are usually added ontop of the language via either external build commands or platform speicfic extesnions. So the language itself is unable to extend itself to these domains, thus these incantations stay on specific compilers and platforms (that is unless a separate standard that all must comply with begins to emerge) with no way to further extend them.

So we need an uniform system which allows us to extend the language using the language itself, we need a way to load the various components others have written and make it our own, writing further abstractions for our projects and libraries. Getting updates lives and instant as the abstractions aren't tacked onto the language, but rather in real time as you develop and put together your program.

For this we need an image!

## Mission Statement / Key Features
1. Live documentation
- we can have our documentation tool update in real time as one writes functions, types, macros, etc.
- We can even give more information as users extend this functionality, as they have access to the same tools we do!
2. Build system
- We can have our build tool be in the language itself, as we have primitives for loading etc. So we can query and reload the code in current time in the project itself, thus leading to less down time.
3. Dependency Management
- We can load new packages in our project's repl, and query for
- So we can do things like filter the packages by various information without having to connect through other processes or figuring out what is available on **this** lts through web calls.
4. Proof Assistant
- The Proof assistant can easily work off the information in the image.
- It can even generate new modules with counter examples using existing functonality of the language!
5. Theorem Prover extesnions
- Users can override our default theorem prover, and provide their own, abstracting over ours or making their own from scratch.
- For reference, SLY/SLIME the lisp editing enviornment does this for debugging giving nice user interfaces for restarts, etc!
6. A restart system
- With our system it'll be easy to have various restarts (via effects!) where we can save from any error or have our machine automatically try restart capabilities!
7. Remote development
- With this model, you can remotely deploy/develop and patch/develop easily, just need to write an SSH library in the language, and bam!
8. Blockchain ingestion
- We could load a blockchain into the image (depending on the size we may want to load stubs of it!), then start exploring it with the image viewer. We could thus call all the code in the mdoules, and simulate contracts on the chain and have a very easy path to testing contracts on live data
9.

Image System Goals
==================

Research Areas
==============

Images are as old as computation, with the Lisp 1.5 compiler being an
image which wrote to and read from a magnetic strip (source required).
However there is very little literature on the subject. [This was a list
of resources we were able to collect about the
subject](https://github.com/heliaxdev/juvix/issues/742). Further, since
the technique has fallen out of fashion in the past few decades, there
are many areas we can explore on this front

First Class Environments
------------------------

First class environments are a way of making the environment code lives
in first class. This means we could talk about discrete environments and
more easily distinguish between startup, compilation time, evaluation
time, etc environments. There are many bigger implications as well, like
being able to talk about environments over the network, having sandboxed
environments, etc.

While the benefits are quite promising, the technique seems to suffer
from a lack of research. There is the
[SICL](http://metamodular.com/SICL/environments.pdf) paper that talks
about adding it to Common Lisp, and the `SBCL` compiler which at it\'s
bootstrapping phase works on creating it\'s own environment. There is
also [MIT
scheme](https://groups.csail.mit.edu/mac/ftpdir/scheme-7.4/doc-html/scheme_14.html)
which has first class environments

With Juvix, we can explore these ideas a lot further, as we have many
systems which facilitate this kind of reasoning. Three particular
constraints come together for this.

1. We have an algebraic effects system
- This is very significant for making progress, as we can see
precisely how our effects touch the image. If we can determine
that, we can likely create a system that can precisely denote
the scope of the image we need to reason over.
- With that said, we need to be careful with our thoughts here, as
free variables are an effect that are discharged by the default
handler. Meaning that if the system fully throws this
information away as it can lookup in the image what answers are
bound to and throw away what it relies upon in the image to
function, then this will be harder to manage.
2. We have multiple backends we must support in a single program.
- This means that we already have to tackle the issue of some
parts of our language being out of scope.
- We are likely to include parts of Racket\'s `#lang` research,
which should help talking about environments on a module level.
3. We have a first class module system.
- We might be able to formalize this idea as our module system, or
view it as an extension of our module system.
- After all the image is one big module!

If we are able to synthesize 1., 2., and 3. properly along with our type
system, we should have a very ergonomic way of creating very eloquent
systems that can talk about library versioning, backend support, and
evaluation time processing.

### Possible Benefits

1. Talk formally about the various environments
- Boot Strapping environment
- Evaluation Environment
- Compilation Environment
2. Better Integration with Block chains
- We could ingest Anoma data into the image, and have multiple
different conflicting nets around.
- We can fully explore them as if they were on our live image, and
switch between the environments and see what effect our code
would have on different sets of conflicting data!
3. Give us a formal way to talk about the environment where our type
system gets injected
- The base image will have to not have an image, as that is rather
hairy to do.
- What this gives us is an environment in which we can talk about
everything having a nice type system.
- We can even push this further for other kinds of type
systems ala what Agda does, but as libraries, not baked
in(?)
4. Leads into a Possible packge/versioning system.
- This could give us an LTS model like Haskell has, and maybe even
better as we can have multiple versions on our image that
doesn\'t conflict with each other?

## Useful Resources

- Factor
- [Factor: A Dynamic Stack-based Programming Language](https://factor-language.blogspot.com/2010/01/factors-bootstrap-process-explained.html)
- Talks about the bootstrapping process along with linking factors core files
- http://factorcode.org/littledan/dls.pdf
- section 3 and below seems useful.
- They talk about how to give an appearce of late binding so they can have inlining but be very flexible. I suspect this resource will give us insight on how to handle local open clashes as time goes on.
- Small Talk
- http://ftp.squeak.org/docs/OOPSLA.Squeak.html
- Talks about the Squeaks compiler and their various decisions.
- Common Lisp
- SBCL
- [SBCL: a Sanely-Bootstrappable Common Lisp](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.144.4124&rep=rep1&type=pdf)
- Talks about the usage of images of CL in the modern day
- lays out their compiler process
- doesn't really talk about making an image, but layous out their process on how they boostrap, may be useful
- SICL
- [SICL: first class environments](http://metamodular.com/SICL/environments.pdf)
- [Clostrum, their more doucmented library work](http://metamodular.com/clostrum.pdf)
- [Call site optimizaoitns](http://metamodular.com/SICL/call-site-optimization.pdf)
- Fast way to remove indirection through the cell most of the time. Fastest of the 3 given here.
- Forth
- GForth
- https://www.complang.tuwien.ac.at/forth/gforth/Docs-html/Image-Files.html
- Not too useful, but the page on image file background has some information.
- Scheme
- MIT Scheme
- In MIT scheme they call images bands
- [First class environments](https://groups.csail.mit.edu/mac/ftpdir/scheme-7.4/doc-html/scheme_14.html)
- [More documentation on how their system works](https://git.savannah.gnu.org/cgit/mit-scheme.git/tree/src/compiler/documentation/porting.guide#n3663)
- [1987: Maybe Scheme style isn't the best!?](http://groups.csail.mit.edu/mac/ftpdir/scheme-mail/HTML/rrrs-1987/msg00135.html)
- [Saving and Loading Images C code](https://git.savannah.gnu.org/cgit/mit-scheme.git/tree/src/microcode/fasdump.c#n509)
- C source
- this is how they save and load the images
- [fasl load format](https://git.savannah.gnu.org/cgit/mit-scheme.git/tree/src/microcode/fasload.c)
- fasl C code
- [fasl](https://git.savannah.gnu.org/cgit/mit-scheme.git/tree/src/microcode/fasl.c)
- More C source
- [fasdump](https://git.savannah.gnu.org/cgit/mit-scheme.git/tree/src/microcode/fasdump.c)
- C source
- Seems Scheme Images/Bands are just FASL dumps!?
- [Saving the image](https://github.com/jaseemabid/mit-scheme/blob/master/src/runtime/savres.scm)
- Scheme Source
- Seems this is how they save the image
- [Free variables and first-class environments](https://link.springer.com/article/10.1007/BF01813016)

- Books
- [Lisp System Implementation](http://t3x.org/lsi/index.html)
- [Lisp From Nothing](http://t3x.org/lfn/index.html)