damienstanton

structure Box α where
  val: α

namespace Box

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

end Box

def a := Box.mk 42

damienstanton

Type theory (Thorsten Altenkirch)

Functions

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

open import Data.Nat

f : ℕ → ℕ

damienstanton

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

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

damienstanton

(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

damienstanton

// 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

damienstanton

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

damienstanton

I := λx.x

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

Idiot := I


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

damienstanton

// 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);

damienstanton

{--
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

damienstanton

Nix builder for Kubernetes

Table of Contents

• Nix builder for Kubernetes
  • Overview
  • Why?
• How?