Adding the 'Type' type

[iacore]

@lpil Sorry about spamming the issue comment section. I am not invested in Gleam enough to write a language proposal, so I'll write down my thoughts now.

The idea is that, a language with Hindley-Milner type system usually use different syntax for terms and types. For example, in Rust:

struct C<T> {
    ...
}

fn c(t: ...) -> ... {
    ...
}

In languages with dependent types, it's different. For example, in Zig:

fn c(t: ...) ... {
    ...
}

fn C(comptime T: type) type {
    ...
}

I think this is too large of a change (if it were a language proposal) for Gleam.

[lpil]

Sorry, what are you suggesting here?

[lpil]

If you have ideas in future do share! This is a very interesting area and there could be some useful things we could benefit from here.

[iacore]

If you are interested, you can try out Idris2 or Lean4. Their tutorials are much better at teaching the concept of their type system, which I can't do.

[lpil]

I've been dabbling in Idris for a long time! It's a fantastic language. Though I've not tried Idris 2 yet.

I'm not asking for you to explain those languages, I'm asking what specifically what addition to Gleam you are proposing.

[iacore]

While I am not much involved with Gleam, I want to see consistent syntax used for types and terms. For example, the syntax for exporting types should be similar to the syntax for exporting terms.

here's a thought:

pub const floats = [1.0, 2.0, 3.0]

pub type MyType = struct { ... }

pub type OtherType = TypeFromOtherModule

For the same reason, I dislike the import _.{type X} syntax. In a sense, types are constants as well:

pub const OtherType: type = TypeFromOtherModule
pub const OtherType = TypeFromOtherModule

Because I am not familiar with Gleam, I do not think I am qualified to give out suggestions like these.

[lpil]

Cool! What new problems could we solve in Gleam with this change that we could not previous?