Hear me out, I’m not advocating for adding declarative constraints or any type algebraic wizardry to the language, I’m rather interested in brainstorming and standardizing the notion for structural, declarative types commonly arising in static analysis. A semi-related example (also canonicalized by the compiler as of now) is anonymous union tags in the form of @TypeOf(U).@"union".tag_type.?. In my ZLS fork, I denote non-fully-resolved integer types in the form of @Int(<signedness>,<bits>) (e.g. an unsigned integer with unknown bits is denoted as @Int(.unsigned,?)), which I consider to be much nicer to work with than a blunt (unknown type). What’s the most interesting and challenging is anytype, which is essentially a comptime duck type. Theoretically a language server can extract the “shape” and type requirements of an anytype argument out of its use site, but there’s no canonical way to encode the extracted requirements into a DX-friendly format. It’s certainly possible to dump all the comptime checks related to the anytype argument to the output and call it a day, but this won’t be terribly useful for call-site diagnostics.
Any thoughts on semi-formalizing the latent semantics of Zig?
2 Likes
I’d be all for it, for example recently I’ve forked the zig compiler, and added a json dump in between Sema/Zcu to be able to implement a callgraph graph representation, and honestly it would have been better if there was a way to really querry deeply the compiler, rather than forking it, because there’s probably zero chance this gets upstreamed. So plus one on that, anything which helps getting more info out of zig will always be useful, for 3rd party tooling. I think programming language tools is such an underutilize space, there’s probably thousands of tools graphical or terminal interface that could be used. For example
this is a snapshot of the zig compiler, and all the dependency of all the callers/callee (including comptime code) this kind of stuff isn’t readily accessible, so currently you have to use the compiler to do that. I would be cool if zig could expose some form of very verbose representation, that any third party tool could use, in order to elevate the zig programming experience, without having to do some hacking.
btw for those curious, all the big squares, are print/log or derivates functions.
5 Likes
Yours is wonderful work! But actually I think you’re looking for something subtly different, which is more like an IR? I’m ideating a human-facing pseudo-Zig that can capture the AST-based, polymorphic projection out of the operational semantics of Zig. For the record, ZLS’ “either type” just scratches the surface of Zig’s latent semantics.
1 Like
Oh so you want a superset which is outside of zig ? and not dependent on the internals of the compiler ?
Yeah, it’s a natural consequence of Zig’s language design, the love-hate operational comptime. While the compilation graph always work with closed-world, monomorphic semantics, language tools, most notably language servers, have to conjure “ghost”, open-world, polymorphic semantics for the AST nodes. I want to provide diagnostics for the call sites of a generic function, but the Zig language doesn’t provide a concise formalism to describe comptime duck typing. I understand and support the decision for keeping declarative contracts out of the language, but the inherent complexity of comptime duck typing must be tamed somewhere in order to provide useful diagnostics.
2 Likes
Agree, but I think it’s better if it stays in the compiler, not out, I think first it will benefit more people, and I think it’s the best place to be, otherwise if every tool needs it’s own analyzer and parser etc, that’s redundant, wasteful, and potentially can lead to issues if all the parsers or analyzer don’t agree, and it’s a lot of work to maintain parity. But i like your idea, I think you should try to explore it, there’s some work being done. Maybe you could try to fork zig and see what you can do, it would be cool
1 Like
I’d want formal semantics for AIR. Despite the claim that it hasn’t fully stabilized yet, the core that is needed for formal analysis doesn’t see a lot of churn.
1 Like
You nailed it. It’s what I actually wanted to ask in another post, but probably due to my unclear rhetorics my core message got largely ignored. It’d be nice if the compiler would eventually go for extra miles for 3rd party language tools in terms of static analysis, however I’m not sure the compiler would bent that much to also cater for the polymorphic semantics a language server needs, say, lazy evaluation in generic type resolution such that a placeholder comptime parameter wouldn’t cause a compile error. Doing so would mean the compiler has to assume the role of a full static analyser, I’m not sure if it resonates with the vision of the core team.
Meanwhile, I’d like to lightly clarify that my proposed declarative superset of Zig (if it’d ever be a thing) would be purely denotational. That means the language wouldn’t have a compiler and it would be for human consumption only. 
1 Like
