Dependent Type Ref Counting

Stream: lean4

[Mac]

How do dependent types work with reference counting? Consider the following example:

constant ContextPtr : PointedType
def ContextRef := ContextPtr.type
instance : Inhabited ContextRef := ⟨ContextPtr.val⟩

@[extern "new_context"]
constant ContextRef.new : IO ContextRef

constant TypePtr (ctx : ContextRef) : PointedType
def TypeRef (ctx : ContextRef) := TypePtr ctx |>.type
instance  {ctx : ContextRef} : Inhabited (TypeRef ctx) := ⟨TypePtr ctx |>.val⟩

@[extern "get_float_type"]
constant getFloatType (ctx : @& ContextRef) : TypeRef ctx

Does get_float_type need to increment ctx reference counter? Does ctx reference counter get decremented during the collection of each of object of TypeRef ctx? How does that work? Does get_float_type need to do anything special to make that happen?

[Mario Carneiro]

Dependent types shouldn't matter at all. The types are all erased in compilation

[Mac]

@Mario Carneiro so how does Lean determine when to garbage collect ctx so that it does not get collected pre-maturely before objects of types depending on it do?

[Mario Carneiro]

get_float_type does not need to increment ctx, because it takes it as borrowed data. If it was owned it would have to decrement ctx

[Mario Carneiro]

That is, it's just as if the type was constant getFloatType (ctx : @& ContextRef) : Unit

[Mario Carneiro]

The only effect of the dependent type is that a ContextRef is going to be forced as an argument to many functions, with all the normal consequences of passing it as an argument

[Mario Carneiro]

Mac said:

Mario Carneiro so how does Lean determine when to garbage collect ctx so that it does not get collected pre-maturely before objects of types depending on it do?

There is no such relation. It can garbage collect ctx once it has finished actually using the data, it doesn't matter if an object of type TypeRef ctx still exists

[Mario Carneiro]

However, if you pass that TypeRef ctx to another function you will have to pass ctx along with it, which will keep it alive

[Mac]

Mario Carneiro said:

However, if you pass that TypeRef ctx to another function you will have to pass ctx along with it, which will keep it alive

But, in many cases, it infers that ctx from the TypeRef ctx object itself?

[Mario Carneiro]

Type inference is orthogonal to all this. The compiler doesn't care if the argument is explicit or implicit