Types in values and values in types

[probeiuscorp]

Types in values

I'd like to have most type annotations exist within expressions, rather than on declarations:

x = x y. Int : x + x * y

I think this is essential to Tilly's identity as an expression oriented language. This approach also works well with having multiple kinds of type annotations, which I think is necessary when there's subtyping. Both of these kinds are so important:

• Satisfies–as: value must satisfy given type. Given type is used as type of whole expression.
• Satisfies: value must satisfy given type. Type of value is used as type of whole expression.

As you might guess from the names, this is very inspired by TypeScript. The syntax of these annotation expressions is tricky, and TypeScript has not the answers for that. These are some considerations for the syntax:

• Type must be on left of value
• Only one of either a separator between the type+value, or a marker before the type, is strictly necessary

However, this is insufficient to replicate ScopedTypeVariables. Types would need to be attached to declarations for that.

Values in types

Either dependent types or typeof.

Dependent types

• Shared namespace.

• Shared evaluation context. Notably the interpretation of literals could benefit from having separate evaluation contexts. I'd like [Int, Int] to evaluate to Cons Int (Cons Int Nil) in a type context. If there was no distinct type context, it'd instead evaluate to [Type, Type] (which is also useful) but is not a type. At a type evaluation context, Cons Int (Cons Int Nil) both is a type and is just as usable for transformation as [Type, Type].

[probeiuscorp]

I'm pretty decided against dependent types. I want the distinct evaluation contexts, and don't want to deal with Type 0, Type 1, Type 2