Re:Idris: A Language for Type-Driven Development
by avgcorrection on Friday January 20, 2023 @05:34PM
(#34461042)
> 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.
Re:Idris: A Language for Type-Driven Development
by brabel on Saturday January 21, 2023 @01:31AM
(#34464387)
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.
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/