Bradley Saul bsaul

LLM Wiki

A pattern for building personal knowledge bases using LLMs.

This is an idea file, it is designed to be copy pasted to your own LLM Agent (e.g. OpenAI Codex, Claude Code, OpenCode / Pi, or etc.). Its goal is to communicate the high level idea, but your agent will build out the specifics in collaboration with you.

The core idea

Most people's experience with LLMs and documents looks like RAG: you upload a collection of files, the LLM retrieves relevant chunks at query time, and generates an answer. This works, but the LLM is rediscovering knowledge from scratch on every question. There's no accumulation. Ask a subtle question that requires synthesizing five documents, and the LLM has to find and piece together the relevant fragments every time. Nothing is built up. NotebookLM, ChatGPT file uploads, and most RAG systems work this way.

Using a Reasonging LLM to find Agda proofs of theorems

As a wee experiment, I've produced a simple Haskell program that sends a prompt containing a lemma to prove in Agda to an LLM. The program checks the LLM-generated proof by invoking Agda, and if the proof contains an error then this is fed back to the LLM and it is asked to try again. This process repeats until a proof passes, or the user aborts (or the LLM reaches some rate limit). The LLMs that I tested were the basic (non-reasoning) models from Claude (e.g. Sonnet 3.7), Llama3 and Llama 4 variants, a version of DeepSeek, a version of Qwen 32B, and the o3 reasoning model from ChatGPT (plus a few others). The experiment here has no human in the loop, the LLM has to produce a totally syntactically correct Agda program which needs to be typed-checked by Agda without any interactive editing or "fix up". The goal here is not to produce a nice proof like one a human might write, but instead to

Haskeller Competency Matrix

See also List of materials about Software Design in Haskell

	Junior	Middle	Senior	Architect
Haskell level	Basic Haskell	Intermediate Haskell	Advanced Haskell	Language-agnostic
Haskell knowledge scope	Learn you a Haskell	Get programming with Haskell	Haskell in Depth	Knows several languages from different categories
	Get programming with Haskell	Haskell in Depth	Functional Design and Architecture
	Soar with Haskell	[Soar

Installation

Easiest, if you have pip:

$ pip install papis

Adding Documents

Most of the time I add documents via their DOI. For example, I'll be on IEEExplore or ResearchGate and see a paper that I either want to read or know for sure I'll want to cite. So I simply copy the DOI and run

Introduction

I was recently asked to explain why I felt disappointed by Haskell, as a language. And, well. Crucified for crucified, I might as well criticise Haskell publicly.

First though, I need to make it explicit that I claim no particular skill with the language - I will in fact vehemently (and convincingly!) argue that I'm a terrible Haskell programmer. And what I'm about to explain is not meant as The Truth, but my current understanding, potentially flawed, incomplete, or flat out incorrect. I welcome any attempt at proving me wrong, because when I dislike something that so many clever people worship, it's usually because I missed an important detail.

Another important point is that this is not meant to convey the idea that Haskell is a bad language. I do feel, however, that the vocal, and sometimes aggressive, reverence in which it's held might lead people to have unreasonable expectations. It certainly was my case, and the reason I'm writing this.

Type classes

I love the concept of type class

(previous Yoneda blog) (reddit) (twitter)

Yoneda Intuition from Humble Beginnings

Let's explore the Yoneda lemma. You don't need to be an advanced Haskeller to understand this. In fact I claim you will understand the first section fine if you're comfortable with map/fmap and id.

I am not out to motivate it, but we will explore Yoneda at the level of terms and at the level of types.

	{-# LANGUAGE TypeSynonymInstances #-}
	data Dual d = D Float d deriving Show
	type Float' = Float

	diff :: (Dual Float' -> Dual Float') -> Float -> Float'
	diff f x = y'
	where D y y' = f (D x 1)

	class VectorSpace v where
	zero :: v

	{- Here is a short demonstration on how to use Agda's solvers that automatically
	prove equations. It seems quite impossible to find complete worked examples
	of how Agda solvers are used.

	Thanks go to @anormalform who helped out with these on Twitter, see
	https://twitter.com/andrejbauer/status/1549693506922364929?s=20&t=7cb1TbB2cspIgktKXU8rng

	I welcome improvements and additions to this file.

	This file works with Agda 2.6.2.2 and standard-library-1.7.1

	{
	"owner": "NixOS",
	"repo": "nixpkgs",
	"rev": "eabe7b845f867e696f8a11be04d47520b3ff4660",
	"sha256": "068qbrp2fvpn437hwg932hm0pav2m10sj7v0kcj3wp8hsvsv088w"
	}

	# Start with all Lepidoptera museum records from
	# Boyle, J., H. Dalgleish, and J. Puzey. 2019a.
	# Data from: Monarch butterfly and milkweed declines substantially predate
	# the use of genetically modified crops. Dryad Digital Repository.
	# https://datadryad.org/resource/doi:10.5061/dryad.sk37gd2

	# these data were downloaded, cleaned, and saved with code provided in Dryad:
	# PART 1.1 Filtering museum data.R
	lep <- readRDS("lep_records.rds")