4 ms·

Zig does some of this. Functions can be written that can be called at compile time or runtime, depending on which language features they use. Types can be com

Zig does some of this. Functions can be written that can be called at compile time or runtime, depending on which language features they use. Types can be computed and returned by functions in compile-time expressions. I don't know how expressive the types can get, though?

Avshalom 4y ago
I'm going to guess not very expressive. Zig refuses to have operator overloading because it might be used to call a function that's more expensive than you'd guess so the idea that they'd let types enforce all that much seems unlikely.
still_grokking 4y ago
You can pass "types" also around in C#… But in both cases that aren't types in the sens of type theory. In both cases those are just regular values (of type "Type"). In both cases you will be able to find those values with the help of a debugger. (The difference between Zig and C# being that in Zig those values are constructed during compilation and than mostly thrown away again whereas the "type" values are just regular runtime data on the CLR).
- skybrian 4y ago
  The types created in compile-time code are just as "real" as the types you declare in source code. All types become values at compile time. When you write a compiler, the parser creates ordinary values, perhaps instances of a Type type. The type-checking code operates on these values to find errors according to the rules of type theory. Compile-time functions are a way of calling user-defined code in the compiler, much like a macro but saner, and they can create types that can be used in declarations, verified by the type checker, and used as input to the code generator. (Reflective use of runtime types in languages like C#, Java, or Go is different.)
  - still_grokking 4y ago
    Even you almost didn't say anything wrong here there is a key misunderstanding: The term "type theory", which I've used and to which I referred (and which you've picked up), is a technical term form math. Languages like C# or Zig are not based on type theory. What is called "types" in those languages has (mostly) no relation to type theory. Those "types" are (mostly) regular values when looked at them through the type theory lens.

Avshalom 4y ago

I'm going to guess not very expressive. Zig refuses to have operator overloading because it might be used to call a function that's more expensive than you'd guess so the idea that they'd let types enforce all that much seems unlikely.

still_grokking 4y ago

You can pass "types" also around in C#… But in both cases that aren't types in the sens of type theory. In both cases those are just regular values (of type "Type"). In both cases you will be able to find those values with the help of a debugger. (The difference between Zig and C# being that in Zig those values are constructed during compilation and than mostly thrown away again whereas the "type" values are just regular runtime data on the CLR).

skybrian 4y ago
The types created in compile-time code are just as "real" as the types you declare in source code. All types become values at compile time. When you write a compiler, the parser creates ordinary values, perhaps instances of a Type type. The type-checking code operates on these values to find errors according to the rules of type theory. Compile-time functions are a way of calling user-defined code in the compiler, much like a macro but saner, and they can create types that can be used in declarations, verified by the type checker, and used as input to the code generator. (Reflective use of runtime types in languages like C#, Java, or Go is different.)
- still_grokking 4y ago
  Even you almost didn't say anything wrong here there is a key misunderstanding: The term "type theory", which I've used and to which I referred (and which you've picked up), is a technical term form math. Languages like C# or Zig are not based on type theory. What is called "types" in those languages has (mostly) no relation to type theory. Those "types" are (mostly) regular values when looked at them through the type theory lens.