The vague idea of a modern dependently-typed programming language.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long. 3.7KB

Ideas for Katrin

Please be aware that at this point this document is just a collection of quite random notes and ideas.



  • Mainly lazy or mainly strict? (→ Haskell/Idris)
    • Probably mainly strict with explicit Lazyness possible (like in Idris) because of performance and algebraic typing
  • Algebraic types
    • Dependently typed
    • How far can we go? Pattern matching types → powerful but drawbacks with free theorems
    • Theorem prover capabilities come with it, but are not the main target
    • Base stuff: Literals, Sets, Tuples
    • Types are (context free? decision problem in polynomial time? should only be a compile-time problem) languages over the Universe where the Universe is the Kleene closure of the set of literals
    • μ-Calculus as theoretical foundation?


Interaction (with users, windows, servers, …) is a very important thing in programming. Unfortunately, it is quite awkward (especially for beginners) in many functional languages. Find better solutions working without loads of monad transformers.

Good GUI solutions are important. Haskell still has no reasonable GUI solutions, which is really hindering adoption. Interaction-oriented language design could help.

  • Actors and Messages: Paralellity (aside from what the compiler can deduce) and interaction through the concept of independent (stateful?) actors communicating through messages. (→ Erlang)
  • Event-driven: Things happening on the outside are represented by events with handlers, maybe IO monads
  • Look into Idris Effects
  • Look into Functional Reactive Programming (→ reactivebanana)
  • katrin shell usable as full command shell (replacing bash etc.) (→ innaytool)
    • Things like piping etc. possible with type-safety
    • How to most elegantly integrate non-Katrin programs?


  • Communication with databases/files/servers/users should easy and type-safe.
  • Implicit typed reading of files (integration with typed file system of CrystalOS)
  • Languages (regular, context-free) at the language heart
    • Probably nonsense


  • Typeclasses are called »traits« (→ Rust)
  • Named trait instances (→ Idris)
  • Infix/Prefix/Custom argument placement (→ Agda)
  • Totality enforced by default (no fromJust, error etc.)

Influenced by

  • Haskell
  • Idris
  • Agda
  • Python
  • Go
  • Rust
  • Erlang

Languages to look into: Lisp, ML, Clojure, F#, Scala, Nix, Nim


Good tooling is very important for a language.

One tool for everything: katrin command line tool is compiler, interpreter, shell, build system, formatter etc. in a single convenient place, like with Go.

  • katrin compile test.katrin compiles a single file into a binary.
  • katrin shell test.katrin starts an interactive shell with the file loaded. Just katrin starts a blank shell.
  • katrin run test.katrin or simply katrin test.katrin executes the file.
  • katrin build builds a project following the directions in the project.yaml file.
  • katrin test runs a Katrin test suite.
  • katrin fmt test.katrin formats a source file following the standardized coding conventions and an optional custom format specification.
  • katrin lint test.katrin gives hints on how to improve a source file.
  • katrin language-server starts a language server for editors supporting the protocol.

YAML files are used for configuration.


  • Unicode syntax or not? (→ here)
  • do-notation?