[historyloop]

I wanna see a language where the type system and the actual language are the same language.

I'm not talking about self-hosted compiler, which TS is already. But basically what runs statically and what is compiled for runtime to be the same language in two contexts.

C++ is moving in that direction with constexpr expansion, but it also has to carry the legacy of macros, its existing type system, templates, and so on.

We need something clean.

[tomsmeding]

This sounds to me like dependently-typed languages might fit the bill. Look at Agda (more fancy-features focused) or Idris (more real-world programming focused).

Their idea is that you can lift value-level computations to the type level one-to-one. This allows you to do tricks with them that are normally only reserved for type-level things: things like equality proofs that are verified at compile time. In fact, the main reason why dependently-typed languages are developed is to exploit the Curry-Howard correspondence saying that every first-order logic statement corresponds to a _type_ in a dependently-typed language, and the validity of the statement is equivalent to the existence of an inhabitant of that corresponding type (= a value that has that type). This allows you to prove arbitrary properties about the functions in your program without ever leaving your programming languages!

Maybe not exactly what you were looking for, but it technically fits your bill :)

[carnitine]

Curry-Howard isn’t that specific, nor do dependent types correspond to first-order logic. Curry-Howard is a broad correspondence between logics and type theories. System F, which is weaker than dependent type theory corresponds to higher-order logic. First-order logic actually doesn’t actually correspond to a popular type system, though the correspondence of course exists.

[benrbray]

Dependently-typed languages often work this way! See for instance "Inductively Defined Propositions" in Coq. (remembering, of course, that propositions are types [2], which proof assistants take quite literally)

[1] https://softwarefoundations.cis.upenn.edu/lf-current/IndProp... [2] https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as...

[IshKebab]

You mean like Zig's compile time manipulation of types? It's very powerful but the problem is it makes it harder for IDEs to reason about code.

[rogerclark]

Check out Circle, a C++ compiler for a superset of C++ that supports regular code at compile time: https://www.circle-lang.org/

[rtpg]

Totally agree. I think that something that has some sort of "partial" evaluation and basically merging values and types would be so powerful and crush many interesting bugs.

Instead of having to do type-level programming, how about relying on the fact that the type checker is also running on a computing machine? The fact that we don't even have super simple stuff like first-class union types (let alone nice type manipulation logic) in most stuff is really painful.

An aside: I think one way Typescript gets away with this (beyond soundness stuff), is that it doesn't have to actually build some high performance evaluation model for its type system. It doesn't care, it's here to check the validity of your code, not to run it! It's a very powerful concept that opened up so much without having to futz about with like... how to efficiently represent all these unions.

How many times have you stared at a thing, think "if I could open up the compiler/type checker at the end, I could totally verify some property of my code, but it is not expressible in the type system"?

[lifthrasiir]

As others have mentioned (only partially though, hence this summary), there are several ways (with varying trade-offs) to achieve this.

Multi-stage programming languages have, well, multiple stages of compilation and you can manipulate types as a first-class value in higher stages. This is a natural extension to the type-level evaluation, as the only thing changes is that the type-level evaluation uses the same fragment of language as the value-level evaluation. Of course we would then have a type of types, a type of types of types and so on; some languages do not distinguish them and a single meta-type is used as catch-all. This model is powerful but you wouldn't get stronger guarantees for lower stages; in particular this model is not a substitute for generic types which typically guarantee that every instance of a generic type is instantiable.

(By the way it is a common misconception that being able to use something like `function f<T>() { return T.size; }` is a first-class type; the type parameter T and the lowered value T is a different thing in different stages.)

Dependently typed languages extend the type system itself to handle mixed types and values. This can be much more huge undertaking than multi-staged programming and harder to reconcile with the type inference and other goodies typically available for strong (enough) type systems, but correctly done they can provide a very strong guarantee that was only possible with static analyses to the limited extent. Note that dependent typing is historically associated with proof assistants but still possible without them; its usefulness and usability would be limited though. (You might have guessed but this is why I don't think dependent typing at the current stage is not the future.)

Conventional metaprogramming methods like macros or code generation are huge wrenches always available for throwing. (Multi-stage programming is also a kind of metaprogramming, but not included in the colloquial "metaprogramming".) They would be significantly limited in scope and/or inconvenient to use, but depending on the scope they might be still appropriate.

[tylorr]

Jai being developed by Jonathan Blow is like that https://inductive.no/jai/

[lifthrasiir]

I really don't like Jai's presentation because there is essentially no text material is available and thus much harder to discuss anything. For the posteriority the actual demonstration is available here [1]; it shows that it is a multi-staged compilation model like Zig, which is very useful and also quite limited.

[1] https://youtu.be/iVN3LLf4wMg?t=1903 (or, seek to 31:43)

[astrange]

The language in my head has an effect system, a proof assistant, lets you run code at compile time iff you prove it to be total and pure, and lets you generate new code and proofs with it. This is just dependent types (and it's similar to Jai and Rust) but I think you could market them in a more imperative way to make them usable.

Oh and typestates instead of OOP.

[crubier]

You mean zig ? https://ziglang.org/

[rscho]

Like this?

https://www.google.com/url?sa=t&source=web&rct=j&url=https:/...

https://www.google.com/url?sa=t&source=web&rct=j&url=https:/...

[lioeters]

Without the Google middleware:

Type Systems as Macros - https://www.ccs.neu.edu/home/stchang/pubs/ckg-popl2017.pdf (PDF)

Stephen Chang, Michael Ballantyne, Milo Turner, and William J. Bowman. 2020. Dependent Type Systems as Macros. Proc. ACM Program. Lang. 4, POPL, Article 3 (January 2020) - https://dl.acm.org/ft_gateway.cfm?id=3371071 (Redirects to download PDF)

> We present Turnstile+, a high-level, macros-based metaDSL for building dependently typed languages

[saagarjha]

Lots of other options provided, but it seems like you may be interested in Lisp.

[jatins]

Ruby's Sorbet? Where type signatures are just Ruby itself with no new syntax. (Not sure if this is what you were looking for though)

[madsbuch]

Idris should also be an example of this.

[kachnuv_ocasek]

Check out any dependently typed language.

[drran]

LISP.

[whateveracct]

Come back in a few years and I'll link you haskell.org ;)