proposal: type system: associative/commutative/keyword types, with/where blocks, type refinement/combinators

[kendfss]

📜 Description

Firstly, wanted to say thanks and congratulations. Heard about this because I was looking for an assembler to build a language on, and yours seems to be that which dreams are made of, respect! If this goes well, we should be able to cover at least #2, #3, and type operators. In general this post is about type reform, but I would appreciate a little more direction on the expectations of the following before beginning an implementation (please don't let this project turn into V by allowing others to push what are effectively bugs into your codebase on purpose, it's okay to ask for help and your projects will be better off if you do instead of letting randos decide what should become of them):

• type operators/arithmetic - I use "type refinement" to describe making types from the intersections of existing types, but with negation (and other combinators) we can take this principle further and design types that qualify as tests. This would complicate the type theory to some extent, but I think these are the sort of tradeoffs that're worth it and will prevent the language from cultivating a leviathan type system like rust (or most of the functional languages I've ever used/seen)
• how do you feel about references on stack and values on heap?
• how do you feel about associativity for serial execution and commutativity for separable execution?
• how do you feel about

I have opinions on all of the above, but am self taught and am sure I've much to learn about them. If this doesn't work out, no hard feelings. I'd be happy to share any fruitful outcomes with this community. I've not yet written any Q so my examples will be quite shoddy. I'm also pulling them from mock ups I wrote for a slightly different syntax, so sorry about the discrepancies.

...

💡 Solution

keyword types

the (semantically) important one is todo (sorry if the name is stupid). This allows you to tell the compiler that you want to give the exact type later; a generics work around. Less importantly I want to make clear that this|that|self, to the extent I've used them, are like keywords. self is the owner of the current scope. that is for arguments to methods that have the same types as owner, only works if there's only one other parameter (vars don't matter here since they're always named) of that type in the method's scope. Just makes it easier to do operator overloads (imo). In principle, these each come with magic methods/attrs like .owner that only get compiled as used.

type extension

we introduce the with keyword as follows

x := []u8 with {path string}

This is my approach to type composition/inheritance (I know roughly how they're different, I'm not sure which I want yet, so it prolly doesn't matter that much lol). I like this approach because you can extend the builtin types without having to sacrifice the things that make them convenient to use without ugly workarounds (though I guess languages like go could just be more proactive about things like that)

type restriction

we introduce the where keyword as follows

x := []todo where { len(self) > 60 } // x is instantiated as a type
y := x(int){1, 2, 3} // fails

This is essentially just sugar for functions of self that return booleans. But we could add more clauses to further restrict the state of permitted values of this type, which could make for a friendly way to design modular test suites. The nice thing is that as far as the parser's concerned with|where are basically just infix/binary operators for type definition objects. Which I guess can lend itself to supporting #4 (recursion), though I guess there are legitimate reasons to leave that out; should be fine if we can define Y-combinators.

type refinement

Again, this is about constructing new types from intersections of old ones. The old types will be named types or their negations

x, y, z := ty{buf []int, path string}, ty{buf []int, path string, char rune}, ty []int & string & !rune
println(typeis(x{}, z)) // true
println(typeis(y{}, z)) // false

we could also allow things like

fn succ(n num !inf) n {
    return n + 1
} // the return type is inferred from the type of n; some finite numeral type

Here z is a signature/anonymous type. We could do similarly for functions, here's a sketch

io := fn ([]todo)(int, error) // guess we could drop the fn to fall in line, kinda starts to look like a lisp though
write := (dst []byte) (n int, err error) {
  pass
}
println(typeis(write, io)) // true

commutative types

cty name { pass }

the difference between these and the other structs is that the underlying memory representation is determined by the compiler. If you don't use any of a type's parameters, it should be omitted from inclusion in the memory layout.

associative types

These are more like the structs we're familiar with because the layout in text is the same as the layout in memory, probably less secure but seems like one of the things people who know when to use it will hate you for leaving it out. If you're uncertain, note that Go structs have this behaviour; shuffling the order of elements can actually change the size of the type in memory; that's a disappointing feature but the sort of thing I'm willing to assume is a worthy optimization for the time being.

effective interfaces

If we allow structs to have default field values, the ones that have no defaults become interfaces. To be clear, these are syntactic/semiotic interfaces. They have no baring on memory layout. But if we do it right, we should be able to suggest smaller interfaces for user functions. We'd probably also need a hoogle equivalent in order to make the most of that, but I think that should be a mandatory feature of all languages. It shouldn't be hard to do it without forcing people's compilers to phone home all the time. May be slightly harder to support enterprise workflows without doing that though; I'm definitely more in the fuck 'em camp, everybody already bends over backwards to give them the best stuff for fear of homelessness/starvation lol.

...

🤔 Alternatives

see #2, #3, and #4 ...

lastly, if the ideas sound any good, let me know of any syntax change you'd like and I'll do my best. Let me know if you want more detailed examples/demos. Or even questions, I haven't really talked much about these ideas to anybody before, maybe you know better ways to skin these proverbial cats. Thanks for your patience, sorry for any bugs, and look forward to learning from the responses!