TheNumbat

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.

Yeah, I'm aware, but wanted to avoid the complexity.

> And there is no reason to limit oneself this way for performance, because again dynamic + erased has no overhead.

Not entirely, since Syl uses static data to describe types' runtime layout. Allowing dynamic there would require overhead (e.g. a uniform representation).

That said, there's not a good reason to prevent types from ever mentioning dynamic values. I didn't include it in the post as I haven't entirely thought it through, but with OxCaml-style modalities, you should be able to mention runtime data in types under a dynamic modality.

> Those language features are not examples of dependent types

They are dependent in the sense that types can depend on (compile-time) values, but indeed they're not conventionally dependent types. I mentioned them because they're popular features that can be implemented with compile-time dependent types.

> But I guess you mean that Syl implement dependent types them with no overhead, like no dictionary passing.

Yes. In 2LTT terms, the meta language is dependently typed, the object language is simply typed, and all types are erased at runtime.

Indeed, it says that because we don't have a library of NEON intrinsics (like ocaml_simd_sse) yet, but the extension itself works.

Yeah, this would be great! Currently only 128-bit SSE/NEON is working but AVX is coming very soon. There's also nothing blocking Windows, but it will require some work. (I added the SIMD support in OxCaml)

See footnote 3.

Yes - upcoming posts will cover the uniqueness and data-race-freedom designs.