You can do that in Smalltalk descendants, if by types you mean metaclasses.

No, types are not runtime values!

That's the whole point.

That's why dependent types are so special (and complicated): You can use them as first class constructs without them being runtime values ever. Everything happens in the type checker.

At runtime there are no types in proper static languages; things like Java / C# are actually quite dynamic in contrast; the dynamic nature was even part of the marketing of those languages back than. (Runtime) reflection is just dynamic typing…

"Runtime value" is an implementation detail. You could write an Idris interpreter.

It'd be useful too. Why should your whole project fail to run just because one file that's not going to get used has a type error?

> "Runtime value" is an implementation detail. You could write an Idris interpreter.

Sure. And such an interpreter would still not interpret types at runtime, as types are not (runtime) values.

Only at type-checking time (which is of course a phase before the program actually runs / gets interpreted) you would do anything with the types.

> It'd be useful too. Why should your whole project fail to run just because one file that's not going to get used has a type error?

Whether that would be anyhow "useful" depends on the definition of "file usage".

If there's any reference form the "used" parts of the program to the "unused file" you have a problem:

A type error (in a language where "programs as proves" is a thing) means that you "proved" false. But form a "prove" of false you can "prove" anything! So you actually lost all proving power. Your program may now explode at runtime with arbitrary type errors anywhere. At that point your "static type system" becomes completely useless.

(Of course, if nothing in your "unused file" is referenced anywhere in the "used" files, noting happens. But in this case that "unused file" isn't part of your program, so it's completely irrelevant what's inside anyway.)

Terra is a language that can also do that, and uses Lua as the metaprogramming language. Types are just Lua values.

But unfortunately, there's a lot of work left kind of half-baked so using the language is a pain... if someone invested a lot of time to make Terra work properly and added some tooling around it, wrote proper docs and so on, it would be a really interesting language.

https://terralang.org/

> Terra is a language that can also do that, and uses Lua as the metaprogramming language. Types are just Lua values.

But then Terra doesn’t do that. Lua does. But not to itself, so it’s not really about passing around types as first-class values any more than metaprogramming Java in Python would elevate Java types to being first-class values.

Terra programs are kind of embedded in Lua, you can't separate the two. So to be very precise: Terra has metaprogramming done via Lua at compile-time, with Terra types being Lua values you can pass around, transform, return etc. in the metaprogramming "layer" of the Terra program.

In Zig, you do the metaprogramming in Zig itself, but you're also limited somewhat as you can only use the comptime "layer" of the program. In my mind, it's very similar.

That claim doesn't look correct.

Zig is just doing "compile time reflection". That's not even remotely close to dependent types.

The whole point of DT is that computed types can be used for type checking, and not only to compute values form them.

DT enable to reason about programs as mathematical proves. That's not possible in Zig, afaik.

If merely passing around values called "types" would be similar to what Idris does every language with runtime reflection and also all dynamic(!) languages would have DT. That's of course not true.