James Sandridge radicaljims

Monads and delimited control are very closely related, so it isn’t too hard to understand them in terms of one another. From a monadic point of view, the big idea is that if you have the computation m >>= f, then f is m’s continuation. It’s the function that is called with m’s result to continue execution after m returns.

If you have a long chain of binds, the continuation is just the composition of all of them. So, for example, if you have

m >>= f >>= g >>= h

then the continuation of m is f >=> g >=> h. Likewise, the continuation of m >>= f is g >=> h.

A quadratic space is a real vector space V with a quadratic form Q(x), e.g. V = R^n with Q as the squared length. The Clifford algebra Cl(V) of a quadratic space is the associative algebra that contains V and satisfies x^2 = Q(x) for all x in V. We're imposing by fiat that the square of a vector should be the quadratic form's value and seeing where it takes us. Treat x^2 = Q(x) as a symbolic rewriting rule that lets you replace x^2 or x x with Q(x) and vice versa whenever x is a vector. Beyond that Cl(V) satisfies the standard axioms of an algebra: it lets you multiply by scalars, it's associative and distributive, but not necessarily commutative.

Remarkably, this is all you need to derive everything about Clifford algebras.

Let me show you how easy it is to bootstrap the theory from nothing.

We know Cl(V) contains a copy of V. Since x^2 = Q(x) for all x, it must also contain a copy of some nonnegative reals.

	{-# OPTIONS --without-K --safe #-}

	open import Categories.Category.Core
	open import Categories.Category.Cartesian

	module Categories.Tactic.Cartesian.Solver {o ℓ e} {𝒞 : Category o ℓ e} (cartesian : Cartesian 𝒞) where

	open import Level

	open import Categories.Category.BinaryProducts

	Here's a block of code in some imaginary assembly language:

	jmp A
	block1
	jmp A
	block2
	jmp A
	block3
	.A ...

	struct AbstractMatrix {
	int m; // number of rows
	int n; // number of columns

	// Pack block at ib, jb of size mb, nb into dest in row-major format.
	virtual void pack_rowmajor(int ib, int jb, int mb, int nb, float *dest) const = 0;

	// Unpack row-major matrix from src into block at ib, jb of size mb, nb.
	virtual void unpack_rowmajor(int ib, int jb, int mb, int nb, const float *src) = 0;

	/*
	transpose_ij (10000x5000): gmemops=0.23, min=0.436734, avg=0.455368, relerr=3.42%
	transpose_ji (10000x5000): gmemops=0.28, min=0.356635, avg=0.363628, relerr=2.55%
	transpose_ij_ij (10000x5000): gmemops=1.53, min=0.065207, avg=0.069465, relerr=6.07%
	transpose_rec1 (10000x5000): gmemops=1.44, min=0.069258, avg=0.075378, relerr=8.96%
	transpose_rec2 (10000x5000): gmemops=1.37, min=0.072819, avg=0.079644, relerr=8.77%

	transpose_ij (100000x100): gmemops=1.70, min=0.011731, avg=0.014102, relerr=9.99%
	transpose_ji (100000x100): gmemops=0.23, min=0.086909, avg=0.095706, relerr=3.37%
	transpose_ij_ij (100000x100): gmemops=1.73, min=0.011543, avg=0.013170, relerr=6.96%

	;; Small example of pseudo-algebraic effects in Racket
	#lang racket

	(define handler-tag (make-continuation-prompt-tag 'handler))

	;; Handler
	(define ((handler x) k)
	(displayln (format "giving back value ~a" x))
	(call-with-continuation-prompt
	(lambda () (k x))

	# This is to be used with catkin_make or catkin_tools if we want to merge compile_commands.txt in a single file to allow some tools to work such as Sourcetail.

	sudo apt install jq

	jq -s 'map(.[])' PATH_TO_COMPILE_COMMANDS_ROOT/**/compile_commands.json > compile_commands.json

	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE UndecidableInstances #-}
	{-# LANGUAGE UnsaturatedTypeFamilies #-}

	import GHC.TypeLits
	import Prelude hiding (Functor, Semigroup)

	type Main = (Fizz <> Buzz) <$> (0 `To` 100)