damienstanton

/*

A type `Nat` is either
   -> Zero
   -> Succ of Nat
 
We can say the same thing in C# 12 (.Net 8)

*/

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

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?

damienstanton

Note that this is meant to be a common subset of useful types, not an exhaustive list.

prelude

• Box<T>, casually referred to as a 'box', provides the simplest form of heap allocation in Rust. Boxes provide ownership for this allocation, and drop their contents when they go out of scope. Boxes also ensure that they never allocate more than isize::MAX bytes.

std::sync

• Arc: Atomically Reference-Counted pointer, which can be used in multithreaded environments to prolong the lifetime of some data until all the threads have finished using it.
• Barrier: Ensures multiple threads will wait for each other to reach a point in the program, before continuing execution all together.
• Condvar: Condition Variable, providing the ability to block a thread while waiting for an event to occur.
• mpsc: Multi-producer, single-consumer queues (channels), used for message-based communication. Can provide a lightweight inter-thread synchronisation mechanism, at the cost of some extra memory.

damienstanton

"Higher-kinded types" is a vague term, conflating multiple language features under a single banner, which can be inaccurate.

As background, this RFC includes a brief overview of the notion of kinds and kindedness. Kinds are often called 'the type of a type,' the exact sort of unhelpful description that only makes sense to someone who already understands what is being explained. Instead, let's try to understand kinds by analogy to types.

In a well-typed language, every expression has a type. Many expressions have what are sometimes called 'base types,' types which are primitive to the language and which cannot be described in terms of other types. In Rust, the types bool, i64, usize, and char are all prominent examples of base types.

In contrast, there are types which are formed by arranging other types - functions are a good example of this. Consider this simple function:

fn not(x: bool) -> bool {

damienstanton

import Foundation

extension String {
    /// Returns the minimum number of bits required to encode the given string
    func bitFloor() -> Int { Int(entropy().rounded(.up)) }
    
    /// Returns the metric entropy of the given string, as a measure of randomness
    func randomness() -> Double { entropy() / Double(self.count)}
    
    /// Returns the approximate Shannon entropy of the given string