# rspl Heapless

This example explores the viability of an alternative implementation of rspl based on something like closure conversion to avoid the use of a heap.
Such an implementation would make rspl better suited for embedded systems as it could not only forgo the standard library but also an allocator.
In the rest of this file we explain and implement that heapless approach to draw a tentative conclusion on its viability.

rspl uses the heap essentially for laziness when it thunks stream processing and tails of streams.
This is because in those cases Rust does not statically determine the size of the thunks.
Assisting Rust in that regard by converting those closures eliminates the need for a heap.\
What we mean by converting closures here can be understood by looking at the example of streams as codata[^1].
In Agda one defines streams of type `X` (intensionally) by the codata type
```agda
record StreamX : Set where
  coinductive
  field
    head : X
    tail : StreamX
```
This can be read as 'any object from which one can observe something of type `X` (the `head`) and a something of type `StreamX` (the `tail`) is a `StreamX`'.
Defining a stream of `X`s can then be done by copatttern matching, that is, by specifying what the `head` and the `tail` of the stream shall be.
For example, given some `x : X` one can construct the constant stream of `x` by the comatch
```agda
constant : X -> StreamX
head (constant x) = x
tail (constant x) = constant x
```
Now, to encode `constant` in Rust one can convert that generalized closure by making its environment (its domain) explicit by means of a struct (as usual), and implement the `Stream<X>`-trait accordingly:

```rust
trait Stream<X> {
    fn head(&self) -> &X;
    fn tail(self) -> Self;
}

struct ComatchConstant<X> {
    constant: X,
}

impl<X> Stream<X> for ComatchConstant<X> {
    fn head(&self) -> &X {
        &self.constant
    }

    fn tail(self) -> Self {
        self
    }
}
```

This also works in greater generality for mutually recursive codata.
For ordinary stream processors in Agda
```agda
data StreamProcessor : Set where
  get : (A -> StreamProcessor) -> StreamProcessor
  put : B -> LazySP -> StreamProcessor

record LazySP where
  coinductive
  field
    force : StreamProcessor
```
we get the following rspl equivalent (if we also generalize `X -> Y` to the intensional definition of function with the help of codata) in Rust:

```rust
enum StreamProcessor<A, B, F, L>
where
    F: Fun<A, B, F, L>,
    L: LazySP<A, B, F, L>,
{
    Get(F, std::marker::PhantomData<A>),
    Put(B, L),
}

trait Fun<A, B, F, L>
where
    F: Fun<A, B, F, L>,
    L: LazySP<A, B, F, L>,
{
    fn apply(self, a: A) -> StreamProcessor<A, B, F, L>;
}

trait LazySP<A, B, F, L>
where
    F: Fun<A, B, F, L>,
    L: LazySP<A, B, F, L>,
{
    fn force(self) -> StreamProcessor<A, B, F, L>;
}

struct ComatchEval<A, B, S, F, L>
where
    S: Stream<A>,
    F: Fun<A, B, F, L>,
    L: LazySP<A, B, F, L>,
{
    phantom_a: std::marker::PhantomData<A>,
    phantom_f: std::marker::PhantomData<F>,
    stream: S,
    output: B,
    lazy_sp: L,
}

impl<A, B, S, F, L> Stream<B> for ComatchEval<A, B, S, F, L>
where
    A: Clone,
    S: Stream<A>,
    F: Fun<A, B, F, L>,
    L: LazySP<A, B, F, L>,
{
    fn head(&self) -> &B {
        &self.output
    }

    fn tail(mut self) -> Self {
        let sp = self.lazy_sp.force();

        if let StreamProcessor::Get(_, _) = sp {
            self.stream = self.stream.tail();
        }

        StreamProcessor::eval(sp, self.stream)
    }
}

impl<A, B, F, L> StreamProcessor<A, B, F, L>
where
    F: Fun<A, B, F, L>,
    L: LazySP<A, B, F, L>,
{
    fn eval<S: Stream<A>>(mut self, mut stream: S) -> ComatchEval<A, B, S, F, L>
    where
        A: Clone,
    {
        loop {
            match self {
                StreamProcessor::Get(f, _) => {
                    self = f.apply(stream.head().clone());
                    while let StreamProcessor::Get(f, _) = self {
                        stream = stream.tail();
                        self = f.apply(stream.head().clone());
                    }
                    continue;
                }
                StreamProcessor::Put(b, lazy_sp) => {
                    return ComatchEval {
                        phantom_a: std::marker::PhantomData,
                        phantom_f: std::marker::PhantomData,
                        stream,
                        output: b,
                        lazy_sp,
                    }
                }
            }
        }
    }
}
```

Then, for a proof of concept we can reimplement the `map`-combinator and apply it to some stream:

```rust
struct ComatchMap<'a, A: 'a, B: 'a, F>
where
    F: Fn(A) -> B,
{
    a: std::marker::PhantomData<&'a A>,
    b: std::marker::PhantomData<&'a B>,
    function: F,
}

type SPMap<'a, A, B, F> = StreamProcessor<A, B, ComatchMap<'a, A, B, F>, ComatchMap<'a, A, B, F>>;

impl<'a, A, B, F> Fun<A, B, ComatchMap<'a, A, B, F>, ComatchMap<'a, A, B, F>>
    for ComatchMap<'a, A, B, F>
where
    F: Fn(A) -> B,
{
    fn apply(self, a: A) -> SPMap<'a, A, B, F> {
        StreamProcessor::Put((self.function)(a), self)
    }
}

impl<'a, A, B, F> LazySP<A, B, ComatchMap<'a, A, B, F>, ComatchMap<'a, A, B, F>>
    for ComatchMap<'a, A, B, F>
where
    F: Fn(A) -> B,
{
    fn force(self) -> SPMap<'a, A, B, F> {
        map(self.function)
    }
}

const fn map<'a, A: 'a, B: 'a, F>(f: F) -> SPMap<'a, A, B, F>
where
    F: Fn(A) -> B,
{
    StreamProcessor::Get(
        ComatchMap {
            a: std::marker::PhantomData,
            b: std::marker::PhantomData,
            function: f,
        },
        std::marker::PhantomData,
    )
}

fn main() {
    let trues = ComatchConstant { constant: true };

    let mut stream = map(|b: bool| !b).eval(trues);

    for _ in 0..1_000_000 {
        println!("{}", stream.head());
        stream = stream.tail();
    }
}
```

The tentative conclusion is that while the approach seems doable, it has significant negative consequences: stream processors become harder to understand and more tedious to write.
Therefore, the approach is impractical.
At least, without a better language frontend.

[^1]: A modern take on OOP generalizing closures (see e.g. [Codata in Action](https://www.microsoft.com/en-us/research/uploads/prod/2020/01/CoDataInAction.pdf)).