Stream: ideas

Topic: (A) Modest Proposal(s)

Wizard ish (Apr 07 2025 at 21:56):

I had a couple ideas for a couple of things that might be interesting in Roc, and I thought maybe theyre something of value so here they are:

1. Parametric Types as Simple Transformations
While Roc's type system is currently quite simple, such a thing has it's disadvantages. Some of these, like classes, are neccasarry losses, however, there is one thing that I belive has a simple implementation, makes the type system if anything simpler, and on the compiler level would be pretty easy.

The idea is that rather than viewing type aliases as their own special type of value, we view them as, well, tradionatal aliases. That is instead of Pair : (_, _), we write Pair = (_, _). Then, instead of using Pair as a value when type-checking, instead, process any instance of it first, so that the type-checker checks Pair -> Pair as (_, _) -> (_, _), which reduces the complexity of type-checking

In addition, it allows for a form of restricted polymorphism. It does this, as, if, for instancePair = (_, _), we could also write Pair a = (a, a). This is just the same as the above version, except now, we also use a abstraction around a type. However, fundementally, it's still the same thing, the type-checkers would read Pair a -> Pair b as (a, a) -> (b, b)

2. Struct as intersection types, tags as union types

A structure type specifically in Roc bears much resemblence to intersection types. This is true in Roc specifically as, for instance, we can write {name : Str, id : Int}a -> {name : Str, id : Int}a, where we abstract over a possible extension to the struct. However, one could reason that it might be sensible to write {name : Str, id : Int} as {name : Str}{id : Int} using the extension syntax, except this time on a concrete type. That is what the idea would be, instead of modeling structs as a special concept, treat them as things that have collection of properties they must have (there fields having certain types). This means we can model the above {name : Str, id : Int}a -> {name : Str, id : Int}a as {name : Str} & {id : Int} & a -> {name : Str} & {id : Int} & a, where now the extension is just an arbitrary type

Tag unions are, well, generic union types.

3. A couple notes

These aren't proposing a complex dependent type system on Roc. Indeed, the first only requires that types can

1. Pattern match
2. Have expressions with parameters of the type
3. Have applications of those expressions

In addition, performance wise, given this limited system, it is known that if two types are applications of a type with equal parameters, then they must be equal.
In other words, we could have a system where whenever we "apply" a "type function" we would add a note of the value used to produce, so for instance, Pair a -> #(Pair a) (a, a) This would allow us, given the above fact, to note that if we have two values of, say Person a = ..., so long as we something annotated with #(Person x) ..., we know without inspecting the inner term that if x ~ y then #(Person y) ... must type-check. This is nothing more then an optimization point, having, or not having an annotation dosen't change the "theoretical" value of a type (ie, #(Pair a) (a, a) still checks (a, a))

Richard Feldman (Apr 07 2025 at 22:49):

I'm not sure how you're using * here - can you use named type variables instead? :sweat_smile:

Richard Feldman (Apr 07 2025 at 22:49):

Pair : (*, *) isn't valid today, and it also wouldn't be valid if those were named type variables

Wizard ish (Apr 07 2025 at 22:50):

wait it isn't?

Wizard ish (Apr 07 2025 at 22:50):

that makes this a lot more simple then, no need to introduce lexical scope of type vars

Richard Feldman (Apr 07 2025 at 22:50):

and it is already the case that the type-checker "desugars" aliases (e.g. if you make the alias Foo : Str, the only difference between Foo and Str is that we might reference one or the other in error messages)

Wizard ish (Apr 07 2025 at 22:50):

The main point is the parametric part

Richard Feldman (Apr 07 2025 at 22:51):

yeah you also can't use underscores in type aliases, at all :sweat_smile:

Wizard ish (Apr 07 2025 at 22:51):

Wait can you use them in types

Richard Feldman (Apr 07 2025 at 22:51):

yeah but not aliases

Wizard ish (Apr 07 2025 at 22:51):

Perfect example of the utility of this

Richard Feldman (Apr 07 2025 at 22:51):

only named type variables are allowed (no * and no _ at all) in aliases, and all named variables have to appear before the : too

Richard Feldman (Apr 07 2025 at 22:52):

I think this would result in a ton of hidden type variables being instantiated behind the scenes, no? to the point of essentially being subtying

Wizard ish (Apr 07 2025 at 22:52):

but this is a perfect example, if you name Pair you lose abilities

Wizard ish (Apr 07 2025 at 22:53):

you could also not implement the third point, and again, i was mainly not thinking about introduced type vars, although it is a reasonable extension

Wizard ish (Apr 07 2025 at 22:53):

Basically the point of the was that you won't ever lose utility by naming a type

Richard Feldman (Apr 07 2025 at 22:54):

sure, but the costs are not the same

Wizard ish (Apr 07 2025 at 22:55):

in terms of the performance?

Richard Feldman (Apr 07 2025 at 22:55):

in a function's type annotation, using _ just means "the type of this function is unchanged but I'm choosing not to annotate it"

Wizard ish (Apr 07 2025 at 22:55):

wait so they should be * then

Wizard ish (Apr 07 2025 at 22:56):

as in any type

Richard Feldman (Apr 07 2025 at 22:56):

today, _ literally just means "I am choosing not to annotate this part"

Richard Feldman (Apr 07 2025 at 22:56):

it doesn't affect anything in any way

Richard Feldman (Apr 07 2025 at 22:56):

if you do foo : _ that is exactly the same as not annotating foo at all

Wizard ish (Apr 07 2025 at 22:56):

yeah it should be *, then.

Wizard ish (Apr 07 2025 at 22:57):

wait isn't that just the same as *

Richard Feldman (Apr 07 2025 at 22:57):

yeah, so the problem is that allowing * in type aliases has massive downsides

Richard Feldman (Apr 07 2025 at 22:57):

it's the same as saying "you can use type variables in type aliases that you don't have to mention in the name of the alias

Richard Feldman (Apr 07 2025 at 22:57):

"

Wizard ish (Apr 07 2025 at 22:58):

even with this, where it's essientally just as if the user had copy-pasted it

Richard Feldman (Apr 07 2025 at 22:58):

yes, the tradeoffs are super different with aliases

Wizard ish (Apr 07 2025 at 22:58):

but still, that means that there are certain things that can't be aliased

Richard Feldman (Apr 07 2025 at 22:58):

yes, that's correct

Richard Feldman (Apr 07 2025 at 22:58):

because the downsides of allowing that are very serious :big_smile:

Wizard ish (Apr 07 2025 at 22:58):

this plan essientally just makes aliases equivalent to copy-pasting

Wizard ish (Apr 07 2025 at 22:59):

ie, parsing -> type transformation -> type checking -> ... would be the system, where the transform doesn't interact with the checker

Richard Feldman (Apr 07 2025 at 23:01):

I haven't though about how to explain this, and unfortunately I gotta go do kid stuff, but please believe me that this is not a simple idea, it's not a simplification to the type system (it would be a major new source of complexity to the implementation), and the reason that ML family languages going back to the 1970s don't offer this isn't that they didn't think of it, it's that it has major downsides that are being overlooked right now :sweat_smile:

Richard Feldman (Apr 07 2025 at 23:01):

@Ayaz Hafiz might have a good explanation though?

Richard Feldman (Apr 07 2025 at 23:02):

really sorry, gotta run! I'll be back on later though

Wizard ish (Apr 07 2025 at 23:02):

see ya

Wizard ish (Apr 07 2025 at 23:03):

although i would like to point out again how these "type transforms" aren't actually a part of the type checker

Brendan Hansknecht (Apr 08 2025 at 00:39):

I probably am missing something, but 1 feels like how type aliases work today. They are just structural fundamentally and the names don't matter.

Brendan Hansknecht (Apr 08 2025 at 00:41):

For 2, I agree that we should have more power and flexibility with records, it was discussed significantly with the proposals around .. syntax, but that probably could use a concrete design doc at this point cause I'm not sure it is clear what exactly is planned.

Ayaz Hafiz (Apr 08 2025 at 01:40):

when would you want to use an alias with an unbound type variable?

Wizard ish (Apr 08 2025 at 01:40):

So yes, this is how type aliases work, however, iirc, type aliases as of current do not allow arbitrary types, that is, given something of the form

$$a : \Phi [x/t]$$

and

$$b : \Phi [ x/T ] \\ T \equiv t$$

,
the validty of a does not imply the validity of b, even though in almost all type systems, both formal and informal, these do indeed hold (delta-reduction fails)

Wizard ish (Apr 08 2025 at 01:41):

Not one hundred percent sure why that isnt working

Wizard ish (Apr 08 2025 at 01:42):

Ayaz Hafiz said:

when would you want to use an alias with an unbound type variable?

In terms of the very simple type system of Roc, you wouldn't: This primarly deals with parametric, not ad-hoc, polymorphism, although if type aliases are always reducible then if a type can contain type vars then a type alias should be able to contain type vars

Wizard ish (Apr 08 2025 at 01:50):

Brendan Hansknecht said:

For 2, I agree that we should have more power and flexibility with records, it was discussed significantly with the proposals around .. syntax, but that probably could use a concrete design doc at this point cause I'm not sure it is clear what exactly is planned.

Also I might point out that struct types can be paraterized in terms of in terms of their extensions, where that is just a intersection type

Ayaz Hafiz (Apr 08 2025 at 02:33):

im struggling to understand the essence of your proposal, what does it enable that is harder/impossible to express in the current language? the current mechanism of aliases is such that aliases are equivalent to underlying type (equal up to unification), but there are well-formedness rules which mean that you cannot say Pair : c for example.

Wizard ish (Apr 08 2025 at 02:34):

Aliases can’t take parameters

Wizard ish (Apr 08 2025 at 02:34):

Or can they :skull:

Wizard ish (Apr 08 2025 at 02:35):

Wait seriously they can’t currently right

Wizard ish (Apr 08 2025 at 02:35):

I’m not just like losing it… right???

Ayaz Hafiz (Apr 08 2025 at 02:35):

Al c : c is valid

Ayaz Hafiz (Apr 08 2025 at 02:35):

if thats what you mean by parameter

Wizard ish (Apr 08 2025 at 02:36):

:skull::skull::skull: ok im just gonna reconsider my life choices for a moment

Wizard ish (Apr 08 2025 at 02:40):

Ok back from slamming my head against a wall

Wizard ish (Apr 08 2025 at 02:41):

Uhm I do think that maybe the syntax should be changed

Wizard ish (Apr 08 2025 at 02:41):

From ‘:’ to ‘=‘ (like Haskell type aliases) as in highlights the type/term distinction

Wizard ish (Apr 08 2025 at 02:50):

Also had an extension to this idea that I thought was pretty dumb but that’s kinda out the window now so, types that take type functions as args as a form of staging, basically, if we have a type of the form (* -> *), * -> *, say, a transformer, we first hide the details of all type functions, and therefore make it ?, * -> *, we apply with the given args, and then we use the other function to transform

Wizard ish (Apr 08 2025 at 15:15):

Ok because I don’t think anything could have been worse than that suggestion time to suggest something crazy

Wizard ish (Apr 08 2025 at 15:15):

Record types as abilities/typeclasses, except they’re values don’t need to be records

Wizard ish (Apr 08 2025 at 15:24):

Basically the idea is that R0 : {field : t0 } can be thought of as a projection get-field : R0 -> t0 (essientally as a Haskell lenses), however the idea would be to extend these lenses to non-records types, ie, abilities, so, we might model a Show ability as Show a = { show : Str }a, and if we need some type that implements Show, we can do this at either the declaration site, ie GameResult = (Win | Draw | Lose) & { show = … }, or at usage by providing an instance at that time (instances probably wouldn’t be allowed outside due to instance resolution getting very complex). Just a random thought I had, also sorry that the formatting is really poor, I just had this idea and I don’t have access to a computer rn

Brendan Hansknecht (Apr 08 2025 at 16:21):

Just to make sure you are up to date, abilities are going away and being replaced by static dispatch. It actually should allow something similar, but still restricted behind custom types.

Wizard ish (Apr 08 2025 at 16:26):

Yeah I’m really not :skull: on your comment on their not being a formal design think this might be a interesting way to do it

Wizard ish (Apr 08 2025 at 16:28):

Basically the idea would be that types can either be something that describes a single representation (i32), a union or intersection of other types (Num, Records, Enums), or something that describes a runtime erased property of the type (a ability / class)

Wizard ish (Apr 08 2025 at 16:28):

Don’t know how useful that is

Ayaz Hafiz (Apr 08 2025 at 18:33):

the problem is you cannot really do this and also get guaranteed type specialization (monomorphization) without a bunch of machinery and I'm not sure that the machinery can be guaranteed either

Ayaz Hafiz (Apr 08 2025 at 18:34):

"undecidability of semi-unification" is the relevant term

Wizard ish (Apr 08 2025 at 18:34):

(deleted)

Wizard ish (Apr 08 2025 at 18:40):

Not that familiar with it, but why would this need pattern matching?

Wizard ish (Apr 08 2025 at 18:41):

(The records)

Ayaz Hafiz (Apr 08 2025 at 18:44):

not sure i follow the comment re pattern matching

Wizard ish (Apr 08 2025 at 18:55):

Just looking up semi unification it seems to be about applying typing to pattern matching

Wizard ish (Apr 08 2025 at 19:03):

though im not familiar with it

Wizard ish (Apr 08 2025 at 20:53):

am i missing something here?

Wizard ish (Apr 09 2025 at 14:58):

I think the part (if I’m correct) that is being missed is that types aliasing/replacement comes strictly before type inference and checking and that they are not codependent

Wizard ish (Apr 09 2025 at 14:59):

The only thing that would need to be added would be a simple occurs check to make sure types are (co-)recursive

Ayaz Hafiz (Apr 10 2025 at 01:15):

im pretty sure what you're proposing requires arbitrary subtyping comparisons

Ayaz Hafiz (Apr 10 2025 at 01:15):

unless i'm misunderstanding

Ayaz Hafiz (Apr 10 2025 at 01:15):

semiunifcation is about the idea that you cannot decidably answer arbitrary subtyping (and equality) constraints with full inference

Wizard ish (Apr 10 2025 at 01:37):

Ah ok, the thing is that this system of aliasing is separate from the substitution, that is, we apply aliases first and only then type check, so, almost like Zig generics, that it where the generics don’t add much complexity, and this system would add even less due to not requiring a full type runtime. Basically this system would probably end up actually being similar, due to the fact that the type checker dosent need to worry about type functions, as it gets the fully expanded types (unless I’m misunderstanding the problem)

Ayaz Hafiz (Apr 10 2025 at 01:41):

Apologies, I'm having a hard time understanding what the concrete proposal is. If you are suggesting that F a : a (or F a = a, let's ignore syntax for now) gets expanded to just a, this is already done.

Wizard ish (Apr 10 2025 at 01:44):

The proposal is that we go from F a b = (a,b) ; F Int c |> (Int, c) BEFORE it goes to the type checker

Wizard ish (Apr 10 2025 at 02:38):

I think I’m probably missing something

Wizard ish (Apr 10 2025 at 02:39):

Oh sorry I misread your message

Wizard ish (Apr 10 2025 at 02:39):

But it’s not done completly due to the fact free vars can’t be included in aliases

Ayaz Hafiz (Apr 10 2025 at 03:41):

why would you want free variables in aliases?

Wizard ish (Apr 10 2025 at 03:41):

Sudo-Ad hoc polymorphism

Wizard ish (Apr 10 2025 at 03:42):

Which you can have in type sigs

Ayaz Hafiz (Apr 10 2025 at 03:42):

can you give some examples

Wizard ish (Apr 10 2025 at 03:43):

Sure, a Frac is two numbers essientally of the form (a,b), where a and b are arbitrary integral types

Wizard ish (Apr 10 2025 at 03:45):

Or a generic operation on a list-like structure

Ayaz Hafiz (Apr 10 2025 at 03:46):

sorry I'm confused again, can you explain how this would be used specifically? like a function implementation

Wizard ish (Apr 10 2025 at 03:47):

Yes, basically the alias acts almost like a macro

Wizard ish (Apr 10 2025 at 03:48):

So we transform the type using the alias, lexically scoping as necessary, and then check

Ayaz Hafiz (Apr 10 2025 at 03:53):

right but what's an usage of that look like in code

Wizard ish (Apr 10 2025 at 03:53):

The same as type aliases do now

Wizard ish (Apr 10 2025 at 03:53):

Just plug it in

Wizard ish (Apr 10 2025 at 03:54):

So f : Pair Int -> Pair Str |> f : (Int,Int) -> (Str, Str)

Wizard ish (Apr 10 2025 at 03:55):

Oh also another cool potential use case for this (even though I know the faq says no) is HKTs as a hypothetical

Wizard ish (Apr 10 2025 at 03:56):

Because they would just be placing in values in templates, it would be valid to have them, but that’s way too large a scope

Wizard ish (Apr 10 2025 at 03:56):

I think basically this is what if you made the Zig type system functional

Ayaz Hafiz (Apr 10 2025 at 03:59):

f : Pair Int -> Pair Str already works and is equivalent to f : (Int, Int) -> (Str, Str)

Ayaz Hafiz (Apr 10 2025 at 03:59):

i think i'm still missing what the new addition is

Wizard ish (Apr 10 2025 at 04:00):

Well that was in response to what it looks like

Wizard ish (Apr 10 2025 at 04:00):

Mostly just the limited ad hoc polymorphism

Wizard ish (Apr 10 2025 at 04:00):

Which dosent have many use cases

Ayaz Hafiz (Apr 10 2025 at 04:02):

that's what i don't understand. what's an example of code what would take advantage of that/

Wizard ish (Apr 10 2025 at 04:03):

Honestly maybe I’m just tired now (or I was just loopy when I was writing this proposal) but I actually can’t think of one rn :sweat_smile:

Wizard ish (Apr 10 2025 at 04:05):

Oh wait I got one… sort of…

Wizard ish (Apr 10 2025 at 04:05):

Basically it’s super trivial to implement without aliases

Wizard ish (Apr 10 2025 at 04:05):

But

Wizard ish (Apr 10 2025 at 04:05):

List length

Wizard ish (Apr 10 2025 at 04:07):

Oh wait

Wizard ish (Apr 10 2025 at 04:07):

Now I remember

Wizard ish (Apr 10 2025 at 04:10):

Ok so intersection types, we have some type alias Trait a = … something that a must have, then a type GTrait = b & Trait b (a trait object)

Ayaz Hafiz (Apr 10 2025 at 04:15):

what is an example program that uses that though

Ayaz Hafiz (Apr 10 2025 at 04:15):

like in code

Wizard ish (Apr 10 2025 at 04:15):

Rust impl and dyn

Ayaz Hafiz (Apr 10 2025 at 04:17):

but like in Roc how do I use that? Like what is an example function we could write that would take advantage of it

Wizard ish (Apr 10 2025 at 04:18):

Honestly I can’t think of one right now and i don’t want to take any more of your time saying all the things at the edge of my mind, I’ll think about it and see if I can think of any more concrete examples for later

Ayaz Hafiz (Apr 10 2025 at 04:19):

my feedback would be to push more on this. i think without concrete examples or usage patterns it's hard to understand the value.

Wizard ish (Apr 10 2025 at 04:20):

Yeah, but right now I think I might need a little sleep, thanks for the discussion :)

Ayaz Hafiz (Apr 10 2025 at 04:20):

gn

Wizard ish (Apr 10 2025 at 16:44):

So the main thing I’ve been able to think of are objects + a method in those objects, I’ll provide a concrete example of this later, and also, I would like to note GHC has something very similar https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/liberal_type_synonyms.html#extension-LiberalTypeSynonyms

Last updated: Jun 16 2026 at 16:19 UTC