jonascarpay/alloy

alloy's Issues

RFC: A type system for the compile time language

These are some thoughts on typing the compile time language. My background in type theory is limited, and input is welcome.

Why not have a type system

Let's say that the primary purpose of a type system is to reject run time bugs at compile time.
If the compile time language doesn't have any notion of run time, why bother taking on all that extra complexity?
If it throws an error, does it matter if that's during evaluation or type checking?

Why have a type system

There are reasons other than rejecting run time bugs for which you might want a type system.
What benefits you get depends on what features you add, but I think these are examples of reasons that apply for pretty much any type system:

1. Types provide machine-checked documentation of function interfaces. Nix gives pseudo-type signatures in its documentation, which is very useful, even without being machine-checked. I think this shows that there is a clear benefit to having a type system.
2. Types simplify debugging. Anybody who has seen a nix stack trace knows how useless they can be for debugging a lazy, dynamically typed language. Instead, a type error tells you more or less exactly where your expectations stopped lining up with reality.

What would a type system look like

This is a list of scattered thoughts about features that would be nice to have.
The thing that I'm most worried about and would like feedback on is how all these features interact.
The only thing I have experience implementing is System F, and if that has taught me anything it's that even a simple change to your type system can have far-reaching and non-intuitive implications.

Inference

Speaks for itself, we don't want to have to provide types for everything.
This might be a given, but it's is on the list because it's important to keep in mind how inference interacts with other features.

Gradual typing

It's important to note that nix does a lot of things that would actually be extremely tricky to type.
Looking at the type of a value (e.g. isFunction) and then making decisions based on that, for example, or looking at what a function is trying to pattern match on and then filling in those arguments dynamically.
These kinds of hacks can be ugly, but they can also be very useful, and I think it's a good argument for why you would want some escape hatches in the type system similar to TypeScript, instead of having a type system that works for every statement in the language.
One nice advantage that we would have over TypeScript is that we don't sacrifice safety, because again, the type system is just for documentation and debugging.

Polymorphism (polymorphic values)

Self explanatory, we don't want to have to create a new identity function for every type.

There is a question here about what level of polymorphism to go for, i.e. Hindley-Milner or full System F.
In Haskell, this is the difference between regular Haskell and RankNTypes, respectively.
You can't do type inference on full System F, although Haskell gets around this by assuming everything is a rank 1 type unless explicitly given a more general type signature.

Dependent-ish types

The types in the runtime language are values in the compile time language.
Therefore, if we want to integrate the two type systems, we need some degree of dependent types.
This doesn't need to be full dependent types.
The way I understand is that restricting it to just runtime types already might simplify the kind system, and thereby sidestep a lot of the tricky parts of full dependent types.

Linear/uniqueness/substructural types

Like dependent types, this is about (the interaction with) the runtime type system.
In short, it would be really neat if we could add resource tracking, or ATS/Rust-style safety guarantees.
Unfortunately, I have a lot more questions about linear types than answers, so I'm not sure this would even make sense.

Row types

The current design is very attrset-heavy.
It might therefore be useful to have row types, meaning constraints about what fields are present, and what type they have.
One annoyance is that attrsets do double duty as records and maps, which I'm not sure how to express.
(Similarly, lists do double duty as tuples and vectors).

Type Operators (polymorphic types)

With dependent types forming the x-axis, and polymorphism forming the y-axis of the lambda cube, this would be the final z-axis.
Note that this is not the same as type operators in Haskell, these are simply type constructors.
In our case this would be most interesting for lists and maps (also see §Row types).

What could not having a type system look like

There is an opportunity here to do something really unique with the type system, but at the same time it's important to realize that it would entail a massive amount of complexity.
The implementation complexity might not necessarily be that bad if we restrain ourselves to type systems that don't influence the runtime language, since then alternative language implementations could safely choose not to do type checking.
However, the cognitive complexity means that someone picking up the language needs to familiarize themselves with all of these features.
This, again, is somewhat ameliorated by the gradual typing, but we still need to take care that we don't turn into ATS.

Concepts

One possible approach would be to do something like C++'s concepts. Concepts would look like nothing more than boolean guards on function arguments. Consider this example:

# fully annotated System F pseudocode
apply ∀ X Y. (f : X -> Y) (x : X) : Y = f x
# concepts
apply (f : isFunction) x = f x

This has the advantage of being easy to learn compared to a type system, and it can check for properties that are not (easily) expressible in types, like list length.

The disadvantage is that it's not actually a type system, which means that there are many things that it can't check, and doesn't actually get you any power, it's really just special syntax for assertions, same as guards in Haskell.

RFC: Name ideas

There already is a language called alloy, so for now alloy is a code name. Here is where we collect names that it could potentially end up having.

Alloy

Alloy is a pretty neat name. It accentuates the fact that it is something stronger (more resistant to Rust, heh) than the sum of its parts, in this case the compile- and runtime languages.

Forge

Still metalworking related. Neat, because in a way it creates tools for creating programs just as much as it creates programs.

Silcrow

§ is a cool symbol. Apparently, it used to signify bureaucracy, and what are macro languages if not bureaucracy?

CP(S)C

Continuation Passing (Style) C. Not a big fan, but maybe shuffle letters around and there's something there, IDK.