Damien Stanton damienstanton

Type theory (Thorsten Altenkirch)

Functions

Unlike in set theory, functions in type theory are by definition computable.

open import Data.Nat

f : ℕ → ℕ

// Either is an example of a sum type.
enum Either<Left, Right>
{
    Ok(Right),
    Err(Left)
}

// Point is an example of a product type.
type Point = (i64, i64, String);

Nix builder for Kubernetes

Table of Contents

Nix builder for Kubernetes
- Overview
- Why?
How?

	structure Box α where
	val: α

	namespace Box

	def extract (b : Box α) := b.val

	end Box

	def a := Box.mk 42

	# ╔════╗
	# ║ DS ║
	# ╚════╝
	# version: 2025.02

	# section: config
	eval "$(/opt/homebrew/bin/brew shellenv)"
	COMPLETION_WAITING_DOTS="true"
	KEYTIMEOUT=1
	plugins=(git

	(ns user
	(:import (java.util.concurrent Executors)))

	;; Thread factory for virtual threads
	(defn thread-factory [name]
	(-> (Thread/ofVirtual)
	(.name name 0)
	(.factory)))

	;; Define an executor which just produce a new virtual thread for every task

	// This file implements a deep embedding of a typed-DSL in Go. The
	// representation is type-safe (we cannot construct ill-typed terms)
	// and accepts multiple interpretations. The type system of the target
	// language is identity-mapped to the Go type system such that type
	// checking of the DSL is hoisted up to type-checking the Go code that
	// contains the target language expression.
	//
	// Normally this requires either GADTs or higher-rank types. I show
	// that it is possible to encode it in Go, a language which doesn't
	// have GADTs (nor regular ADTs for that matter), nor higher-rank

	{
	"diagnostic.virtualText": true,
	"diagnostic.errorSign": "💣",
	"diagnostic.warningSign": "🚧 ",
	"diagnostic.infoSign": "📘 ",
	"diagnostic.hintSign": "🔎 ",
	"python.linting.mypyEnabled": true,
	"haskell.liquidOn": true,
	"languageserver": {
	"go": {

	I := λx.x

	✅ I tweet = tweet
	✅ I chirp = chirp
	✅ I I = I

	Idiot := I


	Mockingbird := M := ω := λf.ff

	{--
	Some informal notes on the talk Cubical Agda: A Dependently Typed Programming
	Language with Univalence and Higher Inductive Types by Andrea Vezzosi.

	Link: https://youtu.be/AZ8wMIar-_c
	--}

	--- Equality in dependently typed languages like Agda is defined as an inductive
	--- family:
	data _≡_ {A : Set} (x : A) : A → Set where