perceus reference counting - dependent types without a garbage collector?

[apostolis.xe...@gmail.com]

https://www.microsoft.com/en-us/research/uploads/prod/2020/11/perceus-tr-v1.pdf

[Nathan Ringo]

This seems like it relies on non-circular data, which isn't the case in Idris because of codata.

[apostolis.xe...@gmail.com]

Codata are non-circular as well. If there was a circle, it would have a finite diameter, but codata are infinite.

[Nathan Ringo]

ones : Stream Nat
ones = 1 :: ones

generates the JS:

const Main_ones = __lazy(function () {
return {a1: 1n, a2: () => Main_ones()};
});

which is circular

[apostolis.xe...@gmail.com]

Main_ones is a function that produces a stream of ones.

You need to look at the memory as it is evaluated, to check if it is circular.

For example, if we evaluated ones 4 times, the memory would be like this :

{ 1 , { 1 , { 1 , { 1 , ones }}}}  . Now, ones in this memory block is a pointer to the function ones.

if we assume that  that each { _ , _} is a new block of memory that is heap allocated, then each { _ , _} inserts in the first place a number and in the second a pointer to the next block of memory.

The pointers, in this way create a line which is non-circular. if we removed the pointer of ones and instead had a pointer to the first block, that would create a circle.