Type Aliases

[mariari]

A lot of MiniJuvix syntax allows Unicode and non Unicode versions, for example

xy-point : ℕ -> ℕ -> Point;
xy-point x y := from-complex (complex x y);

xy-point' : ℕ → ℕ → Point;
xy-point' x y ≔ from-complex (complex x y);

which is nice, as the user may not be writing from an environment which can easily input Unicode symbols.

however, the same could not be said of types. So in the stdlib there is ℕ, but no Nat.

It would be nice if there could exist such type aliases.

Since types are defined with inductive, which is a very specific term, I propose another keyword

alias Nat = ℕ

However, this has the downside of needing more keywords, and I suspect if there are sugar for records we'd end up with inductive, alias, and record all being keywords, potentially breaking user code when they are added in.

Ideally we could just do all these with a generic word like type instead.

[janmasrovira]

In the near future we will try to extend the current type system
to include simple functions that return a type. What I mean by simple is yet to be precisely defined. However, a function such as the following will certainly be accepted:

Nat : Type;
Nat ≔ ℕ;

This will be enough to have type aliases. However, the unicode problem does not end here. We will (probably) still have constructors that use unicode characters, such as ∷.
Of course, one can define a synonym for it thus:

cons : {A : Type} → A → List A → List A;
cons = (∷);

however cons is a function but not a constructor so it can't be used in patterns. For that, we would need pattern synonyms, which we may support in the future but not soon.

That being said, I think (and we will discuss it more thoroughly when extending the stdlib) that we are commited to using unicode extensively and thus we will develop with the assumption that the user should be able and comfortable with unicode.

[mariari]

In the near future we will try to extend the current type system to include simple functions that return a type. What I mean by simple is yet to be precisely defined. However, a function such as the following will certainly be accepted:

Nat : Type;
Nat ≔ ℕ;

This will be enough to have type aliases. However, the unicode problem does not end here. We will (probably) still have constructors that use unicode characters, such as ∷. Of course, one can define a synonym for it thus:

cons : {A : Type} → A → List A → List A;
cons = (∷);

however cons is a function but not a constructor so it can't be used in patterns. For that, we would need pattern synonyms, which we may support in the future but not soon.

That being said, I think (and we will discuss it more thoroughly when extending the stdlib) that we are commited to using unicode extensively and thus we will develop with the assumption that the user should be able and comfortable with unicode.

I would worry that the syntax of

Nat : Type;
Nat ≔ ℕ;

would give off the wrong impression. Namely that types are values, and thus functions can be used in the same way as the rest of the language in which it can't.

[janmasrovira]

We think that going with the long-term syntax, even though we will not support full dependent types soon, is the best option.