Imperative TypeScript alternative (drastically simpler than TypeScript)

[brillout]

The idea is to allow types to be defined imperatively:

type SomeType<T> = {
  if (T is string)
     return boolean
  if (T is SomeOtherType)
    return string
  return never
}

To-do:

• Create a better example that showcases both how much simpler and how much more powerful imperatively defined types would be.
• Create a new TypeScript feature request for it https://github.com/microsoft/TypeScript/issues. Ideally it is the TypeScript team that would add such feature to TypeScript. Otherwise, someone else will eventually create such imperative TypeScript alternative.

Contribution welcome to work on the to-do list above or even create a simple prototype.

[orenelbaum]

Yes! I love this idea! I think that this could be a major breakthrough. However I don't see TS implementing it any time soon.

[orenelbaum]

This is similar / related to Zig's comptime which I'd also really love to see in JS/TS (but doubt I will anytime soon)

[trusktr]

This would be really great, would make types a lot more readable.

cc @JSMonk (Hegel.js author)

It would be nice if these "type functions" can also declare global types and augmentations, like described in this idea:

microsoft/TypeScript#33818

[cyco130]

Love it. Declarative is easier for some things, imperative is easier for others. A general purpose language should support both in as many contexts as possible.

The D language has a static if construct. While it's not a fully imperative metalanguage, it alone makes template meta-programming a lot more pleasant compared to C++. Andresi Alexandrescu once said it's the foremost feature he wished to see added to C++ (it's not the same as if constexpr, you can't use the latter in template definitions).

Meta-programming and computed types are not the same but related. It's crazy how we keep reinventing Lisp macros in different contexts :)

[brillout]

Original thread: https://forum.rescript-lang.org/t/type-constraints/1931/4.

@jlouis

So the type checker might run for a long time, perhaps not even terminate.

I don't see the problem here. Every program has the risk of becoming too slow, that's something we are all aware of when programming. If anything, we are too worried about it — "premature optimization is the root of all evil".

Anyways, current type checkers arleady have the situation that they can become too slow and need to bail out.

And you open the door for having general logic in the type system.

Isn't that actually a good thing? I would even say that it is precisely what we want. See OP of this thread.

Declarative languages are well suited when you already know the result of what you are specifying. For example, HTML, CSS, simple SQL queries, or, in our case, simple types.

But complex types are most often than not imperative in nature. For example:

type SomeType<T> = {
  if (T is string)
     return boolean
  if (T is SomeOtherType)
    return string
  return never
}

When I specify this type, I do not know whether the type results into a boolean, string or never. Now add a couple more if-branches and it becomes clear that you cannot (realistically) define such types with a declarative language.

SQL is another example; it is notoriously difficult to define SQL queries for complex queries. It's the same reason: trying to use a declarative language for specifying something that is imperative in nature.

[cyco130]

Related: The Zig language has the concept of compile-time functions. These functions can manipulate and construct types in compile-time, with the full expressiveness of the Zig language. Example:

fn max(comptime T: type, a: T, b: T) T {
    return if (a > b) a else b;
}

https://ziglang.org/documentation/0.9.1/#comptime

[jlouis]

My comment is mostly in regards to systems with dependent types. Since such systems have type families indexed by terms of the language, you need to be able to reduce terms in the type checker. Consider, e.g., arrays of a certain size: `Vec 4 float` is a vector with 4 components where each component is a float. But this means your type checker must also be able to handle something like `Vec (1 + 3) float` or even `Vec (2 + 2) f(k)`, where the type is computed by another function. If your programming language is guaranteed to terminate, this is never going to happen. But if you allow infinite loops, you risk never completing the type checking phase. I think that trade-off is a valid one to make. But it does complicate your compiler because it needs to be able to run/reduce terms and it also needs to be able to phase-split into things which can be computed now, and things which can be computed later.

…

On Sat, Feb 26, 2022 at 2:48 PM Rom ***@***.***> wrote: Original thread: https://forum.rescript-lang.org/t/type-constraints/1931/4 . @jlouis <https://github.com/jlouis> So the type checker might run for a long time, perhaps not even terminate. I don't see the problem here. Every program has the risk of becoming too slow, that's something we are all aware of when programming. If anything, we are too worried about it — "premature optimization is the root of all evil". Anyways, current type checkers arleady have the situation that they can become too slow and need to bail out. And you open the door for having general logic in the type system. Isn't that actually a good thing? I would even say that it is precisely what we want. See OP of this thread. Declarative languages are well suited when you already know the result of what you are specifying. For example, HTML, CSS, simple SQL queries, or, in our case, simple types. But complex types are most often than not imperative in nature. For example: type SomeType<T> = { if (T is string) return boolean if (T is SomeOtherType) return string return never } When I specify this type, I do not know whether the type results into a boolean, string or never. Now add a couple more if-branches and it becomes clear that you cannot (realistically) define such types with a declarative language. SQL is another example; it is notoriously difficult to define SQL queries for complex queries. It's the same reason: trying to use a declarative language for specifying something that is imperative in nature. — Reply to this email directly, view it on GitHub <#1 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAABMHZM5OPQBFZFNHIWRUTU5DK3HANCNFSM5KXUHXDQ> . Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you were mentioned.Message ID: ***@***.***>

-- J.

[louwers]

Am I crazy, or is this not that much more difficult:

type Equal<X, Y> = (<T>() => T extends X ? 1 : 2) extends <T>() => T extends Y ? 1 : 2 ? true : false

type IfThisThenThatElse<T, U, V, E> = Equal<T, U> extends true ? V : E

type SomeType<T> = IfThisThenThatElse<T, string, boolean,
  IfThisThenThatElse<T, 'SomeOtherType', string, never>
>

I mean, once you have Equal and IfThisThenThatElse.

I find the declarative nature of TypeScript extremely ergonomic. 🙈

[brillout]

I'd still argue that JavaScript is simpler. Maybe it's just because I'm more used to JavaScript. But familiarity does count in simplicity. E.g. I care a lot that what I design does feel familiar to the user.

Example of what @louwers means: https://github.com/vikejs/telefunc/blob/065a3050c414b4004fc3e7128503a3f723fac86e/telefunc/node/server/shield/codegen/types.ts.

Could one achieve the same example but with types defined with JavaScript (or some other imperative language)? Would the performance be comparable? Have imperative languages fundamental drawbacks over declarative languages? CC @redbar0n.

[redbar0n]

Have imperative languages fundamental drawbacks over declarative languages?

I don’t think so. Even declarative languages are often implemented with imperative languages under-the-hood. The bits have to be moved from somewhere to somewhere else, after all.

Could one achieve the same example but with types defined with JavaScript (or some other imperative language)?

Not sure, but I imagine so, if the language is Turing-complete, and if types are treated as values. Some languages let you use types as values at runtime interchangeably.

[brillout]

New idea.

If only there could be a versatile type system that could be used for all kinds of programming languages.

In principle, I don't see why it shouldn't be possible.

Doing a JS alternative is "easy", but doing a TS alternative is hard. I wonder how much code could be shared between type systems.

So that wasm leads to that cambrian explosion of not-experimental-but-actually-useful languages leading to the death of JS.

[orenelbaum]

Can't wait for it to reach 1.0 in 2467

[mindplay-dk]

@brillout did you ever open an issue?

I've been kicking around this idea for a while myself - I would absolutely love to have complex types I can write in minutes rather than days, and still be able to read them a year later. 😅

[brillout]

I would absolutely love to have complex types I can write in minutes rather than days, and still be able to read them a year later

Exactly.

did you ever open an issue?

No. But it'd be awesome if someone does :-).

[mindplay-dk]

I found this issue already existing:

microsoft/TypeScript#41577

[brillout]

@kaleidawave Curious; what do you think of being able to define types imperatively? Ezno does a lot of type inference but I still think the user has to be able to define complex types? (Btw. I'm the author of vite-plugin-ssr which you may find interesting as it enables you to create a complete Ezno framework with all bells and whistles.)

Edit: Btw. Ezno looks really neat 👀.

[brillout]

@mindplay-dk I love you write up microsoft/TypeScript#41577 (comment) 💯.

[kaleidawave]

@brillout Hmm this is interesting.

With the idea at the top I think you could do something like the following in Ezno:

function predicate(a) {
    if (typeof a === "string") {
        return dynamicBoolean
    } else if (a instanceof OtherType) {
        return dynamicString
    } else {
        throw Err();
    }
}

type SomeType<T> = ReturnType<typeof predicate, T>;

So SomeType is based on what Ezno infers from the function, here in it's declarative form T is string ? boolean : (T extends OtherType ? string : never). There are a few things missing that means this doesn't work today but you get the point. Could add a new variant of the type annotation syntax that de-sugars to this, e.g. type X<T> = imperative { T + 2 }

I will ask though why you want a declarative system though 😂😂

If you are getting that you could add SomeType<T> as the return type to a function to make a exposed function in a library type safe in a consumer, then it would have no effect as source type annotations are only constraints under Ezno.

[redbar0n]

I was made aware of this by @anuraghazra

Turns out that @mistlog has made:

typetype - A programming language designed for typescript type generation.

Example:

import { transform } from "@mistlog/typetype";

const input = `
    type function TypeName = (T) => ^{
        if(T extends string) {
            return "string"
        } else {
            return "number"
        }
    }
`;
const output = transform(input).code;
console.log(output);
// output: type TypeName<T> = T extends string ? "string" : "number";