Design Language Prototype

[EduardoRFS]

This is intended to describe the actual language where users are supposed to be coding aka Teika. The goal is a pragmatic language on top of what #104 allows.

Goals

• Functions
• Fixpoint
• Propagation
• Inference
• Modules
• Primitives
• Extensions
• Macros

[EduardoRFS]

Functions and Fixpoint

Teika is a dependently typed language with support to inductive types, but unlike most theorem prover, the calculus chosen is the Calculus of Construction extended with dependent fixpoints(also known as self types), this is documented in #104 and is currently implemented in Smol.

Functions and fixpoints are all the objects in the core language and eventually everything should be implemented in terms of it and aided by compiler primitives to achieve the desirable user experience and performance.

Post-prototype

Additionally post-prototype fixpoints will have zero computationally power, by tracking erasability, as such functions are the only intended way of computing in Teika and fixpoints are not gonna be directly exposed in the syntax, but instead will need to be introduced through some extension syntax.

[EduardoRFS]

Propagation and Inference

Unification

As an ML, Teika will have unification based inference, the main issue for the prototype is how to do proper generalization and implicit instantiation, as I don't want to think about this right now the current solution is to not do generalization or implicit instantiation, additionally in the post-prototype land some level of higher order unification can be supported to aid on pattern matching.

Propagation

Unlike a traditional ML, Teika support full fledge dependent types and even very dependent types(self types), which means unification based inference is not enough, practical Teika requires propagation, this can easily be achieved but needs to be done carefully, as the expected type cannot be easily be propagated to the return type of a dependent function.

The checking algorithm is likely gonna look something similar to Algorithm J + propagation.

Post-prototype

Generalization and implicit instantiation, are very desirable, but currently there are a couple syntax issues with them.

Higher order unification is also important, while in the general case it is not possible, it works nicely for the simpler cases, maybe even higher order patterns should be allowed, but there is some design to be discussed here as ad-hoc inference makes it harder for the average user to understand, especially when dependent elimination is already hard on them.

[EduardoRFS]

Modules

Teika intends to be the next generation of ML, as such modules are required, in OCaml modules serve mainly two purposes, the job of a namespace and the one of dependent sum types allowing nominal types.

Dependent Types and Subtyping

But a major issue is that Teika supports dependent types, as such any concrete module can be reduced to it's normal form, bypassing nomimal types.

Additionally in OCaml the existentiality is added through a subtyping relationship, this relationship will only be supported post-prototype.

Mostly namespaces and data

So for the prototype modules are gonna be used mostly as namespaces and as records, as they're first-class. For the prototype not even the reordering relationship is supported so { x : Int; y : Int; } is not the same as { y : Int; x : Int'; }.

Post-prototype

Nominal types are an open problem, I do have a couple ideas of how to represent them in the calculus through keys, but it's still something that requires time.

Subtyping is a BIG open problem, I don't know how to represent it properly in the calculus, BUT, it is probably a matter of coming up with a scheme and it can definitely be achieved with an extension to the language.

[EduardoRFS]

Primitives

Due to performance and UX concerns, the prototype will have many primitives, some of them are simple such as data types like String and Float, other's will be more complex and focused on helping typing or compilation.

Frozen Types

Due to the lack of nominal types during the prototype inductive types are going to be quite big, checking equality of those types can be very slow and they can lead to very bad error messages. To avoid that frozen types disable all reductions in such a type, such as beta reduction and let aliasing.

Γ |- A : Type
---------------------
Γ |- @frozen A : Type

Γ |- M : A
--------------------------
Γ |- @freeze M : @frozen A

Γ |- M : @frozen A
--------------------
Γ |- @unfreeze M : A

---------------------------
@unfreeze (@frozen M) === M

Int

Int is a recursive / big data types, so implementing it naively in Teika will probably not be super fast especially without nominal types. And as JavaScript is the initial target supporting it through BigInt is relatively easy.

String

String is also recursive / big data types, additionally it has a very good first-class support from JS, where even equality is preserved(=== behaves nicely). Additionally it is a very useful data type to use on primitives and external interfaces.

[EduardoRFS]

The prototype was never fully implemented, but a lot was learned, so closing this in favor of #198