-
Notifications
You must be signed in to change notification settings - Fork 35
Type System Task Force Meeting Notes 2021
Note-taker: Anders Ågren Thuné
Participants: David Broman, Lars Hummelgren, Oscar Eriksson, Viktor Palmkvist, Linnea Ingmar, Daniel Lunden, Anders Ågren Thuné, Gizem Caylak
First meeting! Yay!
We have created a project board at https://github.com/orgs/miking-lang/projects/2, to collect references, requirements and todos for the type system.
Discussion
We discussed the general goals of the type system in Miking.
-
Viktor gave a short introduction to FreezeML. This is a conservative extension to ML-style types which provides annotation-based support for System F along with type inference, in a simple way. We agreed that this should be the base for the type system.
-
We talked about row polymorphism for records and sum types, which is something we will also likely want. Row polymorphism for recursive sum types is likely a research problem.
-
We shortly mentioned unified collection types, ad-hoc overloading, dependent types and higher-order types (System F Omega).
- Work on UCs has started but is reliant on a type system.
- One candidate for ad-hoc overloading is canonical structures. But we need to decide whether this should be a feature in the core language or not.
- Dependent types would be useful for representing e.g. ranks in the types of tensors. Perhaps we could offer a limited form of dependent types specifically for this purpose?
- Higher-order types is something we likely want, but currently it has low priority.
Conclusions
There are three main parts which require active work going forward.
- Implementing FreezeML-style polymorphism in Miking. Primarily Viktor, Lars, Anders, and David will work on this.
- Formalizing / researching row polymorphism for recursive sum types and records in combination with FreezeML. Primarily Viktor, Lars and David will work on this.
- Investigating how to include dependent types (or some limited variant focusing on indexed in tensors) to support our use cases. Primarily Oscar, Lars, and David will work on this.