Let's Find Ourselves Our Stack Inventory
We have now had a common work group, work space and work shop for a multi-disciplinary software/socioware team for about half a decade. For Project Ouroboros and C@ Ana, we mostly focused on contrasting and comparing the simple and dependent-type theories and finding the right use cases of type theory and categories in real-life systems running at home and in the wild. Here's a bunch of languages and their paradigms, which might also inspire your next codebase, stack or coding style - just as it did for us.
Universal Stack Languages: ABCs to XYZs
Agda
Agda is a dependently typed functional programming language. It has inductive families, which are like Haskell's GADTs. However, they can be indexed by values and not just types. It also has parameterized modules, mixfix operators, Unicode characters, and an interactive Emacs interface (the type checker can assist in the development of your code). Agda is also a proof assistant, it is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. It was originally developed aiming to support a wide range of type theories, but the current version supports dependent types, extensible records, coercive subtyping and universe polymorphism.
Bytecode (Graal VM/JVM/LLVM)
Bytecode is a highly optimized set of instructions designed to be executed by a software interpreter. The most common example of bytecode is Java bytecode, which is interpreted by the Java Virtual Machine (JVM). GraalVM is a high-performance runtime that provides significant improvements in application performance and efficiency which is ideal for cloud environments. It is designed for applications written in JavaScript, Python, Ruby, R, JVM-based languages like Java, Scala, Kotlin, and LLVM-based languages such as C and C++. LLVM on the other hand, is a library that is used to construct, optimize and produce intermediate and/or binary machine code. LLVM can be used as a compiler framework, where you provide the "front end" (parser and lexer) and the "back end" (code that converts LLVM's representation to actual machine code).
C/C++/Carbon
C and C++ are general-purpose programming languages which have been around for over 40 years. C++ is an extension of C, and it provides many additional features, such as classes and objects, which support the Object-Oriented Programming paradigm. This paradigm is useful for organizing large codebases and for creating reusable code. Carbon on the other hand, is a source-to-source programming language designed for writing maintainable and scalable code.
Datalog
Datalog is a declarative logic programming language that is syntactically a subset of Prolog. It is often used as a query language for deductive databases. Its applications in databases include integrity constraint checking, complex event processing, and logic-based B2B integration.
Eiffel
Eiffel is an object-oriented programming language emphasizing the design and construction of high-quality and reusable software. Its model of computation is based on Hoare logic and Meyer's design by contract, where assertions form a contract between subroutines and their callers.
Fortran
Fortran (formerly FORTRAN) is a general-purpose, compiled imperative programming language that is especially suited to numeric computation and scientific computing. It is one of the oldest programming languages still in use.
Gleam (Beam VM)
Gleam is a statically typed functional programming language for building scalable concurrent systems. It compiles to Erlang and runs on the BEAM virtual machine used by Erlang and Elixir.
HaXe
Haxe is a high-level cross-platform multi-paradigm programming language and compiler that can produce applications and source code, for many different computing platforms from one code-base. It is free and open-source software, distributed under the GNU General Public License (GPL) 2.0, and the standard library under the MIT License.
Idris 2
Idris 2 is a purely functional programming language with dependent types, optional lazy evaluation, and features inspired by Haskell and ML. Idris 2 is a complete reimplementation of Idris and is implemented in Idris itself.
Julia
Julia is a high-level, high-performance dynamic language for technical computing. It provides a sophisticated compiler, distributed parallel execution, numerical accuracy, and an extensive mathematical function library. Julia’s Base library, largely written in Julia itself, also integrates mature, best-of-breed open source C and Fortran libraries for linear algebra, random number generation, signal processing, and string processing.
sKotlin (ScalaJS + Kotlin UI monorepos)
Scala.js is a compiler that compiles Scala source code to equivalent Javascript code. That lets you write Scala code that you can run in a web browser. Kotlin provides a safer and more functional paradigm-based approach to using the JVM, Java, and Scala ecosystems.
Lean
Lean is a theorem prover and programming language designed to bridge the gap between interactive and automated theorem proving. It provides a dependent-type theory with a small number of basic axioms and inductive definitions.
Miranda
Miranda is a lazy, purely functional programming language, designed for teaching and research and for specialized industrial applications. It has a strong polymorphic type system and supports higher-order functions.
Nim
Nim is a statically typed, compiled systems programming language. It combines successful concepts from mature languages like Python, Ada and Modula. Its design focuses on efficiency, expressiveness, and elegance (in that order of priority).
OCaml
OCaml is a general-purpose programming language with an emphasis on expressiveness and safety. It is a member of the ML language family, which includes Standard ML and F#. INRIA, a French research institute, has developed and distributed it since 1996.
Prolog
Prolog is a logic programming language associated with artificial intelligence and computational linguistics. It has important role in artificial intelligence. Unlike many other programming languages, Prolog is intended primarily as a declarative programming language: the program logic is expressed in terms of relations, represented as facts and rules.
Q
Q# (pronounced as Q sharp) is a domain-specific programming language used for expressing quantum algorithms. It was initially released to the public by Microsoft as part of the Quantum Development Kit.
Racket (Racket + Rust Backend monorepos)
Racket is a general-purpose, multi-paradigm programming language based on the Scheme dialect of Lisp. It is designed to be a platform for programming language design and implementation. Racket is also used for scripting, computer science education, and research. Rust is a similarly optimized and powerful systems development language with a type-safe approach for accessing system internals and borrowing references politely.
Svelte 5
Svelte is a modern JavaScript compiler that allows you to write easy-to-understand JavaScript code, which is then compiled to highly efficient code that runs in the browser. You can write your code using techniques that make it easy to understand, and Svelte will do the work of translating it into highly efficient code that manipulates the DOM.
Typescript
TypeScript is a statically typed superset of JavaScript that compiles to plain JavaScript. It adds optional types, classes, and modules to JavaScript, and supports tools for large-scale JavaScript applications.
Unison
Unison is a new programming language currently under active development. It's a modern, statically-typed, purely functional language, similar to Haskell, but with the ability to describe entire distributed systems with a single program.
XSLT
XSLT is a language for transforming XML documents into other formats (like transforming XML into HTML). The original document is not changed; rather, a new document is created based on the content of an existing one. XSLT uses XPath to define parts of the source document that should match one or more predefined templates. When a match is found, XSLT transform that part of the source document into the result document.
YAML
YAML (a recursive acronym for "YAML Ain't Markup Language") is a human-readable data-serialization language. It is commonly used for configuration files and in applications where data is being stored or transmitted.
Zig
Zig is a general-purpose programming language and toolchain for maintaining robust, optimal, and reusable software. It is an imperative, statically-typed language designed for robustness, optimality, and maintainability.
