The gptel-litellm module, which depends on the uuidgen library, adds tracking of “"sessions"” for users with a LiteLLM proxy backend — where each GPTel Chat buffer constitutes its own session. What this means is that all requests from the same buffer are grouped under the same session-id in LiteLLM’s interface, for accounting and cost tracking purposes. An example of what [...]

Thanks to some late night pairing with Karthik (author of GPTel), I’m now able to announce that ob-gptel is available and working nicely for all my tests thus far. Some features: Use a #+begin_src gptel block to provide a user prompt to submit to GPTel. Refer to previous named source blocks using :prompt, which will use the content [...]

I’ve been using GPTel a lot lately, for many different tasks, and wanted to start sharing some of the packages I’ve built on top of it to aid my work. The first of these is gptel-prompts, which lets you define entries for gptel-directives using individual files instead of Lisp. Several types of files are supported: Plain text files (Org, [...]

Back in 2006, Dan Piponi wrote about Löb’s theorem and how it can be implemented elegantly in Haskell and used to build a spreadsheet calculator from a very minimal core. Further notes on the Haskell wiki abstract his loeb function further, and offer a bit more insight into how it operates. A few years later, as I was working [...]

I first encountered the “recursion schemes” idea in Haskell while attending an excellent presentation given by Tim Williams in 2013. His ideas in that talk made a deep impression on me, and I resolved to find a way to prove the potential he promised in my own work. Now, the basic idea of recursion schemes goes back at least as [...]

Lately I’ve been working again on my Category Theory formalization in Coq, and just now proved, in a completely general setting, the following statement: Monads are monoid (objects) in the (monoidal) category of endofunctors (which is monoidal with respect to functor composition). The proof, using no axioms, is here. Now, just how much category theory was needed to establish this [...]