logoalt Hacker News

Ericson2314 • yesterday at 10:04 PM • 1 reply • view on HN

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.

Replies

TheNumbat • yesterday at 10:51 PM

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.