Add explicit polymorphism

[SebastianMestre]

Right now, there is no way to explicitly mark anything as polymorphic. There really should be.

I was thinking it could look like this (I made up the syntax for function types. see #226):

first : newvar(a){ (a, a) => a } = fn(x, y) => x;

this should also work.

first := newvar(a){ fn(x : a, y : a) => x };

and some sugar to make it nicer:

first := fn<:a:>(x : a, y : a) => x;

Functionally, newvar expressions would function as a scoped declaration, and evaluate to what's between the braces.

Actually, they wouldn't quite be expressions, because they can appear in type terms. They are more like 'meta expressions', which would be evaluated during ct_eval, I suppose.

[lushoBarlett]

Instead of newvar it would be cooler to use forall. It even has the same amount of letters!

[SebastianMestre]

Instead of newvar it would be cooler to use forall. It even has the same amount of letters!

Well, that was obviously my first idea. But if you think about it, ensuring that the variable really gets generalized makes things trickier. I figured I didn't want to over-promise before knowing how easy that would be.

[lushoBarlett]

I don't understand, you mean that even if we declare it as a variable, it could still be unified with some type by inference?

[SebastianMestre]

I don't understand, you mean that even if we declare it as a variable, it could still be unified with some type by inference?

Precisely.

[SebastianMestre]

Let me expand on that a bit further. Here are some facts:

• When we create a new variable, we put it in the environment, at the current scope.

• A variable that is not in scope when we call generalize will be set as one of the arguments in the resulting polytype. (we call this "getting bound to a qualifier")

• When we unify two free variables, we always make the newer one point to the older one.

The first two facts are just part of how Hindley-Milner works, the last fact is just a detail of our implementation. This implementation detail is key to the efficiency and simplicity of our implementation.

Note that, through unification with a variable that was created beforehand, it is possible to a type variable to 'get outside' of the scope in which it was created -- in an abstract sense. This is not the case -- in a literal sense -- if we make unified variables point to the variable with the broader scope

Failing that, we would end up over-generalizing the types (we actually had this exact problem at some point, which is why it's implemented the way it is), or be forced to check if a variable was unified, directly or indirectly, with any of the variables created in the current scope to determine if it should be generalized (this is in contrast to checking if it is equal to any scope variable, which can be done in constant time through hashing, as we currently do).

---

My point with this is that the current invariant is very nice to have, but very easy to accidentally break if, for instance, we add a type of variable that always needs to get bound to a quantifier.

[lushoBarlett]

I just thought about something, should something like this be possible?

newvar(a) {

f := fn(x) { ... };

var1 : a = f(1);
var2 : a = f(2);

};

[SebastianMestre]

yeh, I had the same idea last night, lol. That'd probably be a good thing.