Skip to content

Instantly share code, notes, and snippets.

View sellout's full-sized avatar
🍌
semper φ

Greg Pfeil sellout

🍌
semper φ
View GitHub Profile
@sellout
sellout / git-gc-branches
Last active January 14, 2023 08:24
Clean up old Git branches
#!/usr/bin/env bash
set -euo pipefail
IFS=$'\n'
## Deletes branches (both local and remote) that have been merged upstream.
function usage () {
echo "Usage:"
echo
echo " $(basename "${BASH_ARGV0}") [-h] [-b DEFAULT_BRANCH] [-u UPSTREAM] [-o ORIGIN]"
@sellout
sellout / pseudo-theme.el
Created January 10, 2023 00:29
Customizing Emacs without writing to custom-file, useful for organizing customizations in various ways.
;; Adapted from jwiegley/use-package#881 and jwiegley/use-package#899.
(defun custom-pseudo-theme-set-variables (theme &rest args)
"This is a utility for managing custom values “outside of” a theme."
(unless (memq theme custom-known-themes)
(custom-declare-theme theme (custom-make-theme-feature theme)))
(prog1
(apply #'custom-theme-set-variables
theme
(let ((comment-addendum (format "(Customized by %s.)" theme)))
(mapcar

So you cloned a repo that mentions Nix …

There is a lot to Nix. We’re not going to get into it here. If you are interested, there is a lot of documentation to explore. For our purposes Nix is a tool that allows you to contribute to a project that uses a development ecosystem you are not invested in.

While there is some initial setup, you don’t need to become invested in Nix to benefit from this aspect of it.

@sellout
sellout / git-worktrees.md
Created October 27, 2022 05:00
Git worktree layout

I use git worktrees a lot, and I’ve been annoyed by the repo itself having effectively a privileged worktree that’s always there (and refuses to let any other worktree check out the branch it’s on). And then not having a good place to put my other worktrees. If I clone to $PROJECTS/this-project, where do I put my worktrees?

  • If I put them in the directory, the worktree directories are scattered among all the files in the clone’s working tree (and I seem to remember git having some issues with worktrees inside a working tree), but
  • if I put them next to the directory, then the worktree names need to be prefixed with the repo name (and if there are repos foo and foo-charts, it’s easy to forget that foo-charts isn’t just a worktree of foo.

So, my projects tended to look like this:

$PROJECT_DIR
├── my-project                           # a repo
│   ├── .git
│   └── ...                              # but also a working tree
-- step>
(abst @ (Pair a) ($fHasRepPair @ a))
`cast` (Sub (D:R:RepPair[0] <a>_N) ->_R <Pair a>_R
:: Coercible (Rep (Pair a) -> Pair a) ((a, a) -> Pair a))
-- result>
. @ (->)
$fCategory->
@ (Pair a)
@ (Pair a)
@ (a, a)
@sellout
sellout / OpClasses.idr
Last active August 20, 2022 01:18
Defining ad-hoc polymorphism using dependently-typed implicits.
-- This illustrates (most of) a new(?) encoding of ad-hoc polymorphism using
-- dependent types and implicits.
--
-- Benefits of this approach:
-- • can have multiple “ambiguous” instances without requiring things like
-- Haskell’s newtypes to distinguish them;
-- • can disambiguate instances with minimal information, rather than having to
-- know some arbitrary instance name as you would with a system like Scala’s
-- implicits;
-- • implementers don’t need to know/provide the full family of instances – they
module OpClassesRepro
record SemigroupRec (t : Type) (op : t -> t -> t) where
constructor SemigroupInfo
associative : (a : t) -> (b : t) -> (c : t) -> (op (op a b) c = op a (op b c))
resolveSemigroup
: {auto associative : (a : t) -> (b : t) -> (c : t) -> (op (op a b) c = op a (op b c))}
-> SemigroupRec t op
resolveSemigroup {associative} = SemigroupInfo associative
$ echo "../dhall-bhat/Field/terms.dhall
Type
../dhall-bhat/Category/Monoidal/Set/cartesian
../dhall-bhat/Function/category
../dhall-bhat/Tuple/functor/pair
(./Ratio/Type ./Int/Type)
(./Ratio/field ./Int/Type ./Int/ring)
" | /nix/store/d1mk2rhfrm9ml3m3hyxdala9s0aygvcd-dhall-1.18.0/bin/dhall
{ add =
λ ( t

fixed-point operators

In general, finds the “fixed point” of some endofunctor, which means some type t, such that f t ~ t. The simplest operator is often called Fix, and takes advantage of a language’s primitive recursion to provide a very straightforward definition:

newtype Fix f = Fix { unfix :: f (Fix f) }

There are some problems with this, however:

  1. most languages provide general recursion (and, in fact, this definition requires it), so such a definition can’t be total; and