Kotlin provides the most advanced tools for creating mobile apps and games,
an excellent reactive declarative UI framework called
Noria,
as well as all the tools needed to create most complex desktop applications,
perfected during the development of
Fleet.
It is precisely the experience working on educational apps, developing and Fleet and contemplating
their architecture that motivated me to devise a series of possible additional improvement directions
for Kotlin.
Structured programming pioneered by ALGOL and
structured concurrency used in Kotlin
illustrate one of the pillars of great programming language design:
endorse correct-by-construction software design, foster clarity and predictability, aid reasoning.
The first two proposals can be seen as an introduction of far-reaching contracts
that both foster correctness by construction and set the stage for statically
verifiable contracts
(see also Usability Barriers for Liquid Types by J. Aldrich et al.):
- Purity, constants, and explicit effects (1 page):
In many cases, high-order functions such as
sortWith(comparator)
only have meaningful behaviour if their arguments are pure functions.
Type-level control over the purity of functions
and data is essential to prevent nonsensical behaviour and dangerous vulnerabilities.
- Resources, lifecycles, and structured concurrency (8 pages):
Kotlin relies on scope-based resource management
but lacks mechanisms to prevent leaking,
guarantee lifecycle safety, and rule out conflicting actions statically.
We devise a mechanism addressing these issues in a manner compatible with and inspired by structured concurrency.
Our approach subsumes Rust’s borrowing and is closely related to Capture Checking in Scala and OxCaml,
but lays more focus on shifting the burden from library users to library developers.
Advanced declarative features and type-safe domain-specific languages further expand
correct-by-construction design:
- Startup and dependency injection (1 page):
Application startup often requires initialization of external
services and components possibly configurable via command-line arguments.
We propose a number of minor language extensions to achieve this with zero boilerplate.
- On type providers for Kotlin (2 pages):
We propose introducing a safe form of type providers – compile-time functions
that synthesize interfaces and type aliases – to greatly improve type-safety of libraries and APIs,
enable very sophisticated type-safe domain-specific languages (DSLs) such as embedded SQL.
- First-class query functions for Kotlin (1 page):
We propose introducing query functions inspired by the recently developed Verse calculus, a
novel approach to deterministic functional logic programming combining the powers of Haskell
and Prolog. In a limited form which is much easier to implement, query functions can extend
SQL-like reactive query languages (see Exposed: Kotlin SQL Framework)
by recursive queries that leverage the power of Datalog while remaining easy to read, understand, and maintain.
Type-driven programming facilitates correct-by-construction design in some of the most complex areas:
- Type classes for Kotlin (2 pages): Ideas on introducing typeclasses in Kotlin way.
- Type families for Kotlin (TBD):
Type families indexed by inductive prototypes enable correct-by-construction design of parsers and interpreters,
as well as type-driven design of complex transformation (e.g. compilation) and analysis
(e.g. typechecking and control-flow analysis) algorithms in general. Typefamilies are vital for a declarative
combinator based biparser framework. With
efficient
incremental declarative biparsers, we will be able to provide
next level IDE infrastructure.
Lastly, we propose semantic and syntactic extensions to reach into areas where Python and Lean currently dominate:
- Literate Kotlin (4 pages):
Literate programming is the ultimate approach for building reliable and maintainable applications and libraries.
Kotlin in its current form is not optimized for literate programming and lags
behind Python when it comes to illustrating ideas in tutorials and research papers.
We develop an alternative syntactic front-end for these usages.
- Academic Kotlin (3 pages):
Literate Kotlin extensions dedicated to applications in computer science and in pure mathematics.
On top of that, these extensions enable a declarative reactive illustration framework based on
and backward compatible with PGF/TikZ
(and ultimately Donald Knuth’s METAFONT), helping to incorporate dynamic illustrations
into interactive textbooks and educational apps.