yangzhixuan’s gists

yangzhixuan / EasierIndices.agda

Created September 28, 2025 13:47

Making working with de Brujin indices easier

	{-
	This file demonstrates a technique for making working with de Bruijn-indexed
	terms easier that I learnt from the paper /The Linearity Monad/ by Jennifer
	Paykin and Steve Zdancewic. After defining well-typed terms `Γ ⊢ τ` using de Bruijn
	indices, we define an auxiliary function `lam` that takes in the variable term explicitly:

	> lam : {V : Type} {Γ : Cxt V} {τ σ : Ty V}
	> → (({Δ : Cxt V} → {{IsExt Δ (Γ , τ)}} → Δ ⊢ τ)
	> → (Γ , τ) ⊢ σ)
	> → Γ ⊢ τ ⇒ σ

yangzhixuan / Test.tex

Created August 6, 2024 16:44

Fine-grain numbered elements/theorems

yangzhixuan / CList.agda

Created April 12, 2024 19:19

Refined Church-encoded lists predicatively


	open import Agda.Builtin.Sigma
	open import Agda.Builtin.Equality

	postulate
	funext : ∀ {a b} {A : Set a} {B : A → Set b} → {f g : (x : A) → B x}
	→ ((x : A) → f x ≡ g x) → f ≡ g

	uip : ∀ {a} {A : Set a} {x y : A} → {p q : x ≡ y} → p ≡ q

yangzhixuan / codeinmath.lhs

Created April 7, 2024 22:16

Using lhs2tex code in mathmode

	\documentclass{article}

	\usepackage{amsmath}

	%include polycode.fmt

	\newenvironment{autohscode}%
	{\relax\ifmmode\expandafter\pmboxed\else\expandafter\plainhscode\fi}%
	{\relax\ifmmode\expandafter\endpmboxed\else\expandafter\endplainhscode\fi}

yangzhixuan / MixAlg.hs

Created January 4, 2024 00:36

Mixing two arbitrary functor algebras (using codensity lifting along the fibration of functor algebras)

	{-# LANGUAGE ImpredicativeTypes #-}
	{-# LANGUAGE GADTs #-}

	data Free f a where
	V :: a -> Free f a
	O :: f (Free f a) -> Free f a

	fold :: Functor f => (a -> c) -> (f c -> c) -> Free f a -> c
	fold k alg (V a) = k a
	fold k alg (O o) = alg (fmap (fold k alg) o)

yangzhixuan / Clocked.hs

Last active June 10, 2023 19:05

Clocked guarded recursion in Haskell

	{-# LANGUAGE DataKinds, ImpredicativeTypes #-}

	-- Clocked guarded corecursion in the style of Atkey and McBride
	-- https://bentnib.org/productive.pdf

	-------- Library code -----------
	data Clock

	newtype Later (k :: Clock) (a :: *) = L a

yangzhixuan / TArray.hs

Created April 21, 2023 11:17

Treap-based array

	import Control.Monad (foldM)
	import Prelude hiding (sum)
	import Control.Monad.Random (MonadRandom(getRandom))

	type Pos = Int

	data TArray = E \| N TArray -- Left subtree
	Int -- Data payload (not position!)
	Int -- Priority
	Int -- Size of the tree

yangzhixuan / agda.sty

Created February 24, 2023 20:05

A customised version of agda.sty with some new features: centred code blocks, italic fonts, etc

	% ----------------------------------------------------------------------
	% Some useful commands when doing highlighting of Agda code in LaTeX.
	% ----------------------------------------------------------------------

	\ProvidesPackage{agda}

	\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox,
	calc, environ, xparse, xkeyval, amsmath}

	% https://tex.stackexchange.com/questions/47576/combining-ifxetex-and-ifluatex-with-the-logical-or-operation

yangzhixuan / ndet.rkt

Created June 4, 2022 08:16

Monadic reflection/reification in Racket using delimited control

	#lang racket

	(require "reflection.rkt")

	; unit : x -> [x]
	(define unit (lambda (x) (cons x '())))

	; bind : [x] -> (x -> [y]) -> [y]
	(define bind (lambda (m f) (apply append (map f m))))

yangzhixuan / AdjointFolds.hs

Last active March 20, 2022 18:28

A Haskell implementation of adjoint folds and some interface for category theory.

	{-# LANGUAGE KindSignatures, GADTs, TypeOperators, TypeFamilies, UndecidableInstances #-}
	{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, FlexibleInstances #-}
	{-# LANGUAGE ConstraintKinds, DeriveFunctor #-}

	import Prelude hiding (Functor)
	import qualified Prelude (Functor)

	-- This file explores doing category theory in Haskell by implementing
	-- Ralf Hinze et al.'s adjoint folds [1]:
	--

Zhixuan Yang yangzhixuan