Comment by Hirrolot | Hacker News Reader

Comment by Hirrolot | Hacker News Reader

Zig is an attempt to merge metaprogramming and type system into a single, coherent unit, however not without drawbacks. Basically, in an ideal language, I see that type system permits three kinds of dependencies:

- Values dependent on values (algorithms)

- Values dependent on types (parametric polymorphism)

- Types dependent on types (type-level functions)

This is one dimension weaker than Calculus of Constructions (CoC) [1], which permits types dependent on values (so-called "dependent types"), but we don't need them until we want to prove some properties about our code (dependent types correspond to logical predicates). Some tasks handled by metaprogramming however may not be handled even by a type system that permits type-level functions; for this reason, probably we have to include some sort of simple syntax transformations, such as those found in Idris [2].

I expatiated in one of my posts [3] on why static languages duplicate their language concepts. This writing also includes Zig and Idris.

[1] https://gist.github.com/Hirrolot/89c60f821270059a09c14b940b4...

[2] http://docs.idris-lang.org/en/latest/tutorial/syntax.html

[3] https://hirrolot.github.io/posts/why-static-languages-suffer...

Thank you for your well written article. It plainly describes thoughts that I've had yet struggled to put concretely in words.

You mentioned the complexities of idris and the lack of adoption for a unified system. Are you hopeful that programming languages will begin to move in this direction, or do you think we will quickly arrive at a "good enough" halfway house (Rust seems like a good example of this)?

I'm afraid I can't answer your question. Either scenario -- a unified system or a "halfway house" -- might be the case; it depends on the intentions of people who design programming languages and the number of pretty arbitrary factors determining their success. But since the general trend is that the PL community is heading towards more advanced type features, maybe someday we should see such a language.

By the way, I don't think it's time to claim that Rust is a "good enough" house -- simply too little time passed since it was embraced by the community. The language didn't even include `async`/`.await` some four years ago. Macros 2.0 are being developed; a new trait solver too. If after some ten or twenty years we'll find it being a mess of legacy, maybe it is not the right way to design a language.

Your record–array correspondence reminded me of Nils Holmes's T3X language: it has "struct" defintions like this:

    STRUCT struct_name = field_1, ..., field_N;

but it's just a syntactic sugar for

    CONST field_1 = 0, ..., field_N = N-1, struct_name = N;

just so that suitably sized vectors can be used as records:

    STRUCT POINT = PX, PY, PCOLOR;   ! same as CONST PX = 0, PY = 1, PCOLOR = 2, POINT = 3;
    VAR    p[POINT];                 ! same as VAR p[3];

    p[PCOLOR] := 42;                 ! same as p[2] := 42;

It works reasonably well and actually allows for somewhat better meta-programming than e.g. C with its X-macros because you can literally loop over a struct's field, in a normal FOR loop.

It seems like this only works with dynamic typing or if you assumed every field was the same width? Otherwise you can't actually specify the widths of each of the struct fields.

I'd think the compiler and language runtime could know the width for any particular offset at access time.

Perhaps TypeScript is a very clean example of the duplication phenomenon you mention in that article, because unlike in most languages, static types are completely erased during compilation. It’s literally a typecheck-time functional programming language bolted onto an existing dynamic runtime language. For some complex object manipulations, the cleanest thing to do is to write two independent recursive functions: a runtime one to compute the value, and a typelevel one to compute the resulting type.

Actually, I think types are erased in most typed languages, unless they support runtime reflection.

Type erasure is a specific compilation technique, it means more than a lack of introspection capabilities.

In most languages, a function taking a float and a function taking an int end up producing different compiler output (because they need to use different CPU registers). More to the point, this extends to generic/template functions with signatures like “void foo<T>(T arg)”, which then need to be monomorphized, that is, copied for each instantiation.

Languages with type erasure simply drop the type argument instead of instantiating it.

What kinds of metaprogramming cannot be expressed via dependent types? AIUI, dependent types potentially dispense completely with the phase separation found in languages like C, so anything can be "evaluated at compile time" simply by writing ordinary programs that make sense within the language itself. Of course sometimes it is desirable to reintroduce a separate "run time" phase, but this can be done via program extraction.

In general, dependently typed systems lack the ability to metaprogram at the syntactic level. This is particularly true we’re binding forms are concerned. The most thoroughly pursued type theoretic way to do this is to implement a modal type system, which is technically orthogonal to the dependency capabilities of the type system, but integration of the two is tricky.

What're the failings of elaborator reflection in providing this in your view? I haven't used it thoroughly, but I thought one could define custom binding forms with it (in Idris 1, at least).

I enjoyed your post, the discussion was thorough and well laid out. Also, your implementation of the lambda cube is very clean and well laid out.

Reply on news.ycombinator.com