Generics

By supporting dependent types, you support generics.

Functions

id[T](x: T) = x
/* Implicitly expanded to: */
id[T: Type](x: T): T = x;

What’s going on here?

1. id is an identifier, just like in x = 5 .
2. [...] denotes an implicit argument. This is an argument the compiler is allowed to implicitly make any value it sees convenient.
3. T: Type is saying T is a Type (this could probably be made more generic).

Defining Types

Pair(A, B) = Struct {
	left: A;
	right: B;
};

What’s going on here?

1. Pair: (Type, Type) -> Type
2. The right hand side is an expression because everything is an expression.
3. What is the constructor which makes types?

Maybe tuples and objects can be interpreted as both a type and a value? I.e (1, 2) and (Int, Int) are both tuples, but you can write (1, 2): (Int, Int).

Could you do something like (1, Int): (Int, Type)?

Is this something special with :? Is it saying “if the two sides have the same constructor, recurse”? Could this cause ambiguities? Could this apply to other constructors? User defined structures?

What about constructors?

Expr: Type where {
	Add(left: Expr, right: Expr): Expr;
	Sub(left: Expr, right: Expr): Expr;
	Const(n: Int): Expr;
};

Expr: Type where {
	Add: (Expr, Expr) -> Expr;
	Sub: (Expr, Expr) -> Expr;
	Const: Int -> Expr;
};