2026-03-30·8 min read·sota.io team

Deploy Idris 2 to Europe — Type-Driven Development with EU Hosting in 2026

In 2006, Edwin Brady began working on a programming language at the University of St Andrews in Scotland. His goal was something that had been theoretically possible for decades but practically absent from production: a language where the type system was powerful enough to express and verify correctness properties of programs — not just whether a value was an integer, but whether that integer was within bounds, whether a list was non-empty, whether a state machine was in a valid state.

The result was Idris, and its successor Idris 2 — redesigned from scratch using Quantitative Type Theory — is the most practically oriented dependently typed language for building real software. Brady is now at the University of Edinburgh 🏴󠁧󠁢󠁳󠁣󠁴󠁿, one of Europe's oldest and most prestigious research universities, where he continues to develop Idris 2 alongside collaborators at the University of Strathclyde 🇬🇧 (Glasgow) and research partners across the European type theory community.

This guide shows how to deploy Idris 2 backends — compiled to native binaries via Chez Scheme — to EU infrastructure with sota.io.

The European Roots of Quantitative Type Theory

Idris 2 is not just another dependently typed language. Its theoretical foundation is Quantitative Type Theory (QTT), developed by Brady and Robert Atkey 🇬🇧 at the University of Strathclyde, with foundational contributions from Conor McBride 🇬🇧 (also Strathclyde). QTT extends standard type theory with resource tracking — types can encode not just what a value is, but how many times it is used. This enables compile-time memory safety without a garbage collector, erasure of proof terms that have no runtime cost, and correct handling of linear resources like file handles or network sockets.

The intellectual lineage is distinctly Scottish and British, rooted in the Glasgow/Strathclyde tradition of type theory:

Conor McBride 🇬🇧 (University of Strathclyde, Glasgow) — one of the most influential figures in practical dependent types. McBride developed the notion of ornaments (structured relationships between datatypes), pioneered the use of universes for generic programming, and co-authored the paper on QTT with Brady. His work on McBride's Epigram language (developed at Durham University 🏴󠁧󠁢󠁥󠁮󠁧󠁿) was a direct precursor to Idris.

Robert Atkey 🇬🇧 (University of Strathclyde, Glasgow) — co-author of the QTT paper (Syntax and Semantics of Quantitative Type Theory, 2018), which gave Idris 2 its theoretical foundation. Atkey's work on parametricity, effect systems, and linear types directly shaped how Idris 2 handles resource tracking and erasure.

Per Martin-Löf 🇸🇪 (Stockholm University) — the foundational layer beneath all dependent type theory. Martin-Löf Type Theory (MLTT), developed in the 1970s–1980s at Stockholm, is the mathematical bedrock on which Agda, Coq, Lean, and Idris all build. Without the Swedish logician's work on constructive mathematics and the propositions-as-types correspondence, none of these languages would exist.

The TYPES Consortium — the EU-funded Types for Proofs and Programs research network has been coordinating dependent type theory research across European institutions since 1992. Current participants include INRIA 🇫🇷, Chalmers 🇸🇪, TU Delft 🇳🇱, University of Edinburgh 🏴󠁧󠁢󠁳󠁣󠁴󠁿, DIKU (Copenhagen) 🇩🇰, and many others. Idris 2 is a direct beneficiary of this sustained European research investment.

Teaching at EU Universities — Idris and Idris 2 are used for teaching type theory, verified programming, and formal methods at Edinburgh 🏴󠁧󠁢󠁳󠁣󠁴󠁿, Strathclyde 🇬🇧, Chalmers 🇸🇪, Utrecht 🇳🇱, and EPFL 🇨🇭. Brady's book Type-Driven Development with Idris (Manning, 2017) is a standard text in European graduate courses on programming language theory.

What Makes Idris 2 Different

Most programming languages separate types and values. In Haskell, the list type is [a] — a list of values of some type a. In Idris 2, the list type can be Vect n a — a list of exactly n values, where n is itself a value computed at compile time. The length is part of the type.

This is called dependent types, and it changes what the compiler can verify:

module SafeList

-- A vector of exactly n elements
-- The length n is in the type, not just a runtime value
head : Vect (S n) a -> a
head (x :: _) = x

-- This compiles — the type guarantees the list is non-empty
example1 : String
example1 = head ["hello", "world"]

-- This would be a COMPILE-TIME ERROR:
-- example2 : String
-- example2 = head []  -- Vect 0 String does not match Vect (S n) String

No null pointer exception. No bounds checking at runtime. The type system enforces non-emptiness statically. The same principle extends to:

State machines — types encode valid state transitions, invalid transitions are compile errors
Protocol correctness — session types guarantee request/response protocols are followed
Resource safety — linear types ensure file handles and database connections are closed exactly once
Format strings — the printf-style format is verified against argument types at compile time

Quantitative annotations are Idris 2's unique contribution. Every binding carries a quantity:

0 — erased at runtime (exists only in types, no runtime cost)
1 — used exactly once (linear, like Rust's ownership)
ω (unrestricted) — can be used any number of times (the default)

-- The proof term `prf` is erased at runtime (quantity 0)
-- It exists only to satisfy the type checker
safeDiv : (n : Nat) -> (d : Nat) -> (0 prf : d = S k) -> Nat
safeDiv n d _ = n `div` d

-- The handle is used exactly once (quantity 1)
-- Prevents double-close or use-after-close
processFile : (1 h : FileHandle) -> IO ()

Building an HTTP Backend in Idris 2

Idris 2's standard library includes Network.Socket for low-level TCP, and the community package idris2-http provides higher-level HTTP handling. Here is a complete backend service:

module Main

import Network.Socket
import Data.String
import System
import System.File

-- Simple HTTP response builder
httpOK : String -> String
httpOK body =
  "HTTP/1.1 200 OK\r\n" ++
  "Content-Type: application/json\r\n" ++
  "Content-Length: " ++ show (length body) ++ "\r\n" ++
  "Connection: close\r\n" ++
  "\r\n" ++
  body

-- Route handler with exhaustive pattern matching
-- The compiler verifies all cases are covered
data Route = Health | Items | NotFound String

parseRoute : String -> Route
parseRoute "/health"    = Health
parseRoute "/api/items" = Items
parseRoute path         = NotFound path

handleRoute : Route -> String
handleRoute Health         = httpOK """{"status": "ok"}"""
handleRoute Items          = httpOK """{"items": ["idris", "types", "proofs"]}"""
handleRoute (NotFound path) =
  "HTTP/1.1 404 Not Found\r\n\r\n" ++
  "{\"error\": \"Not found: " ++ path ++ "\"}"

-- Extract path from HTTP request line
parsePath : String -> String
parsePath req =
  case words req of
    (_ :: path :: _) => path
    _                => "/"

-- Handle a single client connection
handleClient : Socket -> IO ()
handleClient sock = do
  Right (req, _) <- recv sock 4096
    | Left err => putStrLn ("Recv error: " ++ show err)
  let firstLine = case lines req of { (l :: _) => l; [] => "" }
  let path      = parsePath firstLine
  let route     = parseRoute path
  let response  = handleRoute route
  _ <- send sock response
  close sock

-- Main server loop
serve : Socket -> IO ()
serve server = do
  Right (client, _) <- accept server
    | Left err => putStrLn ("Accept error: " ++ show err)
  handleClient client
  serve server

main : IO ()
main = do
  Right sock <- socket AF_INET Stream defaultProtocol
    | Left err => die ("Socket error: " ++ show err)
  Right () <- bind sock (Hostname "0.0.0.0") 8080
    | Left err => die ("Bind error: " ++ show err)
  Right () <- listen sock 10
    | Left err => die ("Listen error: " ++ show err)
  putStrLn "Listening on :8080"
  serve sock

Notice the exhaustive pattern matching in parseRoute and handleRoute. The Idris 2 compiler verifies that every possible case is handled. If you add a new route variant and forget to handle it, the code will not compile. No runtime MatchFailure exceptions.

Packaging for sota.io

Idris 2 compiles to native binaries via Chez Scheme (the default backend) or directly to C. The binary can be deployed as a standalone executable with no runtime dependencies.

Project structure:

myapp/
├── myapp.ipkg          # Idris 2 package manifest
├── src/
│   └── Main.idr        # Application entry point
├── Dockerfile
└── .gitignore

myapp.ipkg:

package myapp

sourcedir = "src"
main = Main
executable = "myapp"

depends = base
        , network

Dockerfile:

FROM ubuntu:24.04 AS builder

# Install Idris 2 and Chez Scheme
RUN apt-get update && apt-get install -y \
    curl \
    git \
    chezscheme \
    libgmp-dev \
    && rm -rf /var/lib/apt/lists/*

# Install Idris 2 from binary release
RUN curl -L https://github.com/idris-lang/Idris2/releases/latest/download/idris2-linux-x86_64.tar.gz \
    | tar -xz -C /usr/local/

WORKDIR /app
COPY myapp.ipkg .
COPY src/ src/

# Build native binary via Chez Scheme
RUN idris2 --build myapp.ipkg

FROM ubuntu:24.04
RUN apt-get update && apt-get install -y libgmp10 && rm -rf /var/lib/apt/lists/*
WORKDIR /app
COPY --from=builder /app/build/exec/myapp .
EXPOSE 8080
CMD ["./myapp"]

Build and push:

docker build -t myapp:latest .
docker tag myapp:latest registry.sota.io/YOUR_PROJECT_ID/myapp:latest
docker push registry.sota.io/YOUR_PROJECT_ID/myapp:latest

Deploy on sota.io:

# Create service from Docker image
sota services create \
  --name myapp \
  --image registry.sota.io/YOUR_PROJECT_ID/myapp:latest \
  --port 8080 \
  --region eu-central

# Check status
sota services status myapp

Your Idris 2 backend is running on EU infrastructure, GDPR-compliant by default.

Why EU Teams Use Idris 2

Formal verification for safety-critical systems. EU regulations increasingly require formal verification for safety-critical software — aerospace (EASA), medical devices (EU MDR 2017/745), railway (EN 50128), automotive (ISO 26262). Idris 2's type system can express and verify safety properties that traditional testing cannot cover. Several European aerospace and defence contractors have explored Idris and Agda for certified software components.

Correctness by construction. Rather than testing that your API does not crash, you can write types that make crashes impossible. For EU FinTech (PSD2 compliance), healthcare (HIPAA/GDPR data flows), and any system where a runtime error has regulatory consequences, Idris 2 offers structural guarantees that dynamically typed or even conventionally typed languages cannot.

European academic collaborations. If your team has members from Edinburgh 🏴󠁧󠁢󠁳󠁣󠁴󠁿, Strathclyde 🇬🇧, Chalmers 🇸🇪, TU Delft 🇳🇱, EPFL 🇨🇭, or INRIA 🇫🇷, they have likely encountered Idris or its academic cousins. The TYPES consortium has seeded dependent type expertise across the continent.

Linear types for resource correctness. Idris 2's 1-quantity annotations enforce linear usage of resources: database connections, file handles, network sockets, cryptographic keys. The compiler verifies that every resource is released exactly once. No resource leaks, no double-free, no use-after-close — verified at compile time, not discovered in production.

Supply chain transparency. Idris 2 is developed at the University of Edinburgh — a public research institution — under the BSD-3 licence. The core contributors are academic researchers, not a single company's engineering team. For EU public sector procurement and open source compliance, the provenance is clean.

Practical Considerations

Ecosystem maturity. Idris 2 is a research language in active development. The standard library is smaller than Haskell's or Rust's. For production use, evaluate whether your requirements can be met by the available packages (idris2-pack has around 150 packages as of 2026).

Compilation times. Dependently typed languages do more work during compilation — the type checker is also a theorem prover. For large projects, expect longer compile times than in languages with simpler type systems. Incremental compilation and caching help significantly.

Learning curve. Idris 2 requires comfort with type theory concepts — dependent types, totality, erasure — that are uncommon in industry backgrounds. Teams coming from Haskell or Agda will adapt quickly; teams from Python or JavaScript should budget time for the conceptual shift. Brady's Type-Driven Development with Idris is the recommended starting point.

When Idris 2 is the right choice:

You need to verify correctness properties that tests cannot exhaustively cover
Safety-critical or regulated systems where formal guarantees reduce certification cost
Protocol-heavy APIs where session types can eliminate a class of integration bugs
Teams with type theory backgrounds looking for a language that matches their training

Deploy on EU Infrastructure

sota.io runs on servers in Germany (Frankfurt) and other EU data centres. Every application is isolated by default, all data stays within EU jurisdiction, and GDPR compliance is structural — not an afterthought.

Get started:

# Install sota CLI
curl -fsSL https://sota.io/install.sh | sh

# Log in
sota login

# Deploy from Dockerfile
sota deploy --port 8080

# Custom domain (optional)
sota domains add idris.yourdomain.eu

Your verified, type-safe backend. Built in Edinburgh. Hosted in Europe.

European Connections Summary

Who	Institution	Contribution
Edwin Brady 🏴󠁧󠁢󠁳󠁣󠁴󠁿	Univ. of Edinburgh / St Andrews	Idris 1 and 2, primary author
Conor McBride 🇬🇧	Univ. of Strathclyde (Glasgow)	QTT foundations, Epigram, ornaments
Robert Atkey 🇬🇧	Univ. of Strathclyde (Glasgow)	QTT paper co-author, parametricity
Per Martin-Löf 🇸🇪	Stockholm University	MLTT — foundational type theory
Thierry Coquand 🇫🇷🇸🇪	INRIA → Chalmers	Calculus of Constructions, CoC→Coq→Agda lineage
TYPES Consortium	EU-wide	Funded type theory research 1992–present

Idris 2 is the practical output of four decades of European mathematics, logic, and programming language research. The language exists because European universities have consistently funded foundational research that does not have immediate commercial applications — and because researchers like Brady, McBride, and Atkey were able to take that theory and turn it into a compiler you can install today.