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. 7.0KB

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 laziness 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? Well, that was a bad idea. Probably.


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)
    • Not sure I like that…
    • Monad typeclasses instead of transformers (MonadIO, PandocMonad…)
  • 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?


In the real-world, working with external data in file systems and databases is one of the most important tasks for programs. It should be easy.

  • Communication with databases/files/servers/users should be 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)
    • Probably a bad idea
  • Totality enforced by default (no fromJust, error etc.)
    • Do the pros outweigh the cons here?

Influenced by

  • Haskell
  • Idris
  • Agda
  • Python: Indentation syntax
  • Go
  • Rust: Trait naming
  • Erlang

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



Good and unified tooling right from the start is very important for a language and its acceptance. Negative Example: Haskell, that wasn’t actually usable before Stack was introduced about 2016 (!)

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

  • katrin compile test.katrin (or katrin c test.katrin) compiles a single file into a binary.
  • katrin shell test1.katrin ... starts an interactive shell with the files loaded. Just katrin shell or 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.
    • Integrate into compile?
  • katrin language-server starts a language server for editors supporting the protocol.

YAML files are used for configuration as they’re especially human-friendly.


Debugging needs to be easy and comprehensive.

The Zen of Katrin

Follow the Zen of Python principles. (?)

  • Nudges (By default, allow only the good stuff, but make anything possible)
  • Modularity (Very small language core for a lean compiler and good forward compatibility)
  • Dry (Don’t repeat yourself)
  • Fancy, but not too fancy (Don’t do stuff just because it looks cool, e.g. Unicode syntax)
  • Question everything


  • Unicode syntax or not? (→ here)
    • Probably not :sad:
    • Only allow a certain set of characters in the code, but Strings are of course Unicode-compatible (it’s the 21st century after all)
    • Might look pretty, but that’s a small gain for the large price of possibly unwritable and unreadable functions flying around
    • Can be overridden
  • do-notation?
  • Are traits/type classes even a good idea? (TODO find article)
    • In general, probably yes.
  • Infix syntax?
  • Allow flexible function syntax like in Agda?
    • Idris has a syntax statement for that, maybe that’s better. Deviating syntax should be disicentivized to keep stuff consistent
    • Something like x <elementOf> list is clearly more expressive than x elementOf list where you can’t know wether x or elementOf is the actual function. And I can’t think of many situations where non-explicit non-standard function application syntax would be a good idea
    • That also poses a lot of problems for the parser
    • if-then-else might be an exception
      • How to handle that? Syntax statement sounds good. Still difficult for the parser
      • Or simply disallow it and do something like `if (a == 0) (print “0”) (print “Not 0”) but that might be less readable
  • Disincentivize special characters only operators. Better <map> than <$> or <parseKey> than .:!
    • Far easier to comprehend.
    • Basic stuff like <$> might still be okay, but then again, <map> really isn’t that much longer (and maybe even easier to type).
    • Prefer meaningful names in general (looking at you, Haskell!).
  • Records in Haskell are deeply flawed. Fix that, they’re really importent in practice! Bring in the dot operator (as some people also did for Haskell).
  • One of the pros of OO-programming is that you can set a paramater for a whole class and then all functions of the class can use that. Without that functions calls sometimes get awkward when you have to pass the same parameters (config, server URL) over and over again. There are ways to alleviate that, maybe find something elegant to integrate into the language?
    • Something like singletons? Constants that can be set on module load? Something like that
    • Stay functional and type-safe of course
    • Maybe dependent types can be useful for this?