Comment by dlahoda
17 hours ago
lean4 unifies types and values, so that types feels so natural. you stop thinking types at all as you think about types in rust or csharp. and haskell does not have that feeling too.
zig may be like that too, but not tried.
Yes. It might sound counter-intuitive or even ironical but the next logical step is to make the type system more, not less expressive and to add completely dependent types. Every language already has them to the extent of Array<T, N> (or T[] & { length: N }, or a recursively defined Tuple<T, N>), but having true flow- and value-dependent types would allow for more concise and expressive code.