- OOP is existential types where the layouts share some sort of shared prefix (e.g. pointer to vtable, fields in common, etc.). To accurately model such things (and they occur in FFI), you need to separate types from layout, and hold the "supertype's layout" fixed.
- A classic use-case of dependent types is dynamically-sized arrays, and "tensors". When you have a pair (L: Nat, V: Pointer(Array(N, T))), you have a layout behind the pointer that is dynamic, but you don't want to conflate this with arbitrary types of the pointee.
Failure to deal with this in fully generality will force you to go down Rust's path of ad-hoc arrays and "dyn trait", which is actually more complexity.
I think those can be modeled without explicitly separating layouts from types (not that doing so is necessarily a bad idea).
For arrays:
let dyn_array = fn (erased t : type) -> record { len : int @@ dynamic, data : pointer(array(len, t)) }
For "dyn trait":
let vtable = fn (erased t : type) -> record { print : pointer(t) -> string, ... }
let dyn_print = record { t : type @@ dynamic erased, vtable : pointer(vtable(t)), data : pointer(t) }
Both use dependent records and the dynamic modality I mentioned above. dyn_print doesn't match C++ since it doesn't inline the data, and giving that a static layout would require parameterizing on the layout of t, so I see your point. However, it might be fine to give dyn_print an "incomplete" layout that can only appear behind a pointer.
let dyn_array = fn (erased t : type) -> record { len : int @@ dynamic, data : pointer(array(len, t)) }
Yes, but array(len, t) has a dynamic layout. Your system needs to understand that that is OK because `pointer(array(len, t))` still has a static layout. You need to understand that pointee-monomorphization is not necessary. You can do special hacks for the `pointer` type constructor, but then you cannot eta-expand it (i.e. wrap in a one field struct). To make this work in a first-class way, so custom data types can have type parameters that do not need to be monomorphized, you need your type system to be layout-aware.
Also, you can do
let dyn_array = fn (dynamic erased t : type) -> record { len : int @@ dynamic, data : pointer(array(len, t)) }
There is no need to force the element type to be static. The array itself doesn't care. The pointee is already dynamic-layout either way.
> [code below]
let vtable = fn (erased t : type) -> record { print : pointer(t) -> string, ... }
let dyn_print = record { t : type @@ dynamic erased, vtable : pointer(vtable(t)), data : pointer(t) }
The problem with this is that `vtable` is being called with a dynamic-erased argument, but it itself requires a static type. That means the whole thing is dynamic (well, depending on exactly how the modalities work). But do want to statically know it is a record with a print field, etc.
> static layout would require parameterizing on the layout of t, so I see your point
I don't think you want to avoid this complexity:
- OOP is existential types where the layouts share some sort of shared prefix (e.g. pointer to vtable, fields in common, etc.). To accurately model such things (and they occur in FFI), you need to separate types from layout, and hold the "supertype's layout" fixed.
- A classic use-case of dependent types is dynamically-sized arrays, and "tensors". When you have a pair (L: Nat, V: Pointer(Array(N, T))), you have a layout behind the pointer that is dynamic, but you don't want to conflate this with arbitrary types of the pointee.
Failure to deal with this in fully generality will force you to go down Rust's path of ad-hoc arrays and "dyn trait", which is actually more complexity.
I think those can be modeled without explicitly separating layouts from types (not that doing so is necessarily a bad idea).
For arrays:
For "dyn trait": Both use dependent records and the dynamic modality I mentioned above. dyn_print doesn't match C++ since it doesn't inline the data, and giving that a static layout would require parameterizing on the layout of t, so I see your point. However, it might be fine to give dyn_print an "incomplete" layout that can only appear behind a pointer.> [code below]
Yes, but array(len, t) has a dynamic layout. Your system needs to understand that that is OK because `pointer(array(len, t))` still has a static layout. You need to understand that pointee-monomorphization is not necessary. You can do special hacks for the `pointer` type constructor, but then you cannot eta-expand it (i.e. wrap in a one field struct). To make this work in a first-class way, so custom data types can have type parameters that do not need to be monomorphized, you need your type system to be layout-aware.Also, you can do
There is no need to force the element type to be static. The array itself doesn't care. The pointee is already dynamic-layout either way.> [code below]
The problem with this is that `vtable` is being called with a dynamic-erased argument, but it itself requires a static type. That means the whole thing is dynamic (well, depending on exactly how the modalities work). But do want to statically know it is a record with a print field, etc.> static layout would require parameterizing on the layout of t, so I see your point
:) See https://docs.rs/stack_dst/latest/stack_dst/ for example, which tries to hack it in Rust. It would be much nicely to do it safely!