Skip to content

Instantly share code, notes, and snippets.

View copumpkin's full-sized avatar
💭
Mostly unresponsive these days

Daniel Peebles copumpkin

💭
Mostly unresponsive these days
View GitHub Profile
@twanvl
twanvl / Sorting.agda
Last active December 2, 2022 16:44
Correctness and runtime of mergesort, insertion sort and selection sort.
module Sorting where
-- See https://www.twanvl.nl/blog/agda/sorting
open import Level using () renaming (zero to ℓ₀;_⊔_ to lmax)
open import Data.List hiding (merge)
open import Data.List.Properties
open import Data.Nat hiding (_≟_;_≤?_)
open import Data.Nat.Properties hiding (_≟_;_≤?_;≤-refl;≤-trans)
open import Data.Nat.Logarithm
open import Data.Nat.Induction
@sjoerdvisscher
sjoerdvisscher / skewbintree.hs
Last active March 18, 2024 17:13
Skew binary tree with the invariants enforced by the type system, using a nested data type.
{-# LANGUAGE GADTs #-}
type Id = Int
data Path a where
P :: P a -> Path a
Two :: b -> b -> P (Br b) -> (P (Br b) -> P a) -> Path a
data Br a = Br a Id a
data P a = Nil | Zero (P (Br a)) | One a (P (Br a))
@copumpkin
copumpkin / Prickler.hs
Last active August 29, 2015 13:57
Reasonably painless bidirectional serialization of sums of products
{-# LANGUAGE TemplateHaskell, ExistentialQuantification, RankNTypes, GADTs, ImplicitParams, TypeFamilies, DataKinds, TypeOperators, DeriveGeneric, PolyKinds #-}
module Prickler where
{-
Main goals:
# Minimal indirection, so I didn't want big n-tuples of stuff getting curried into constructors or shit like that
# Magical constructor/eliminator pairing, so I don't have to write ugly unsafe pattern matches or constructor -> Int mappings (unlike the alt combinator in the pickler paper)
# Minimize the amount of metadata traversal that happens during serialization (not 100% there yet)
# Not be ugly to use
-}
module Matrices
-- Vector stuff ~ maybe put Prelude.Vect
||| Dot product between numerical vectors
dot : Num a => Vect n a -> Vect n a -> a
dot w v = sum (zipWith (*) w v)
||| Numerical vector times a scalar of the appropriate type
@andrejbauer
andrejbauer / topology.v
Last active November 28, 2023 19:40
How to get started with point-set topology in Coq. This is not actually how one would do it, but it is an intuitive setup for a classical mathematician.
(* How do to topology in Coq if you are secretly an HOL fan.
We will not use type classes or canonical structures because they
count as "advanced" technology. But we will use notations.
*)
(* We think of subsets as propositional functions.
Thus, if [A] is a type [x : A] and [U] is a subset of [A],
[U x] means "[x] is an element of [U]".
*)
Definition P (A : Type) := A -> Prop.
@edolstra
edolstra / nix-ui.md
Last active February 2, 2024 23:31
Nix UI

General notes

  • nix-channel and ~/.nix-defexpr are gone. We'll use $NIX_PATH (or user environment specific overrides configured via nix set-path) to look up packages. Since $NIX_PATH supports URLs nowadays, this removes the need for channels: you can just set $NIX_PATH to e.g. https://nixos.org/channels/nixos-15.09/nixexprs.tar.xz and stay up to date automatically.

  • By default, packages are selected by attribute name, rather than the name attribute. Thus nix install hello is basically equivalent to nix-env -iA hello. The attribute name is recorded in the user environment manifest and used in upgrades. Thus (at least by default) hello won't be upgraded to helloVariant.

    @vcunat suggested making this an arbitrary Nix expression rather than an attrpath, e.g. firefox.override { enableFoo = true; }. However, such an expression would not have a key in the user environment, unlike an attrpath. Better to require an explicit flag for this.

TBD: How to deal with search path clashes.

@shortjared
shortjared / list.txt
Last active March 27, 2024 11:19
List of AWS Service Principals
a4b.amazonaws.com
access-analyzer.amazonaws.com
account.amazonaws.com
acm-pca.amazonaws.com
acm.amazonaws.com
airflow-env.amazonaws.com
airflow.amazonaws.com
alexa-appkit.amazon.com
alexa-connectedhome.amazon.com
amazonmq.amazonaws.com
#!/usr/bin/env python
from os import listdir
from os.path import isfile, join
import re
import json
from bs4 import BeautifulSoup
"""
@noamsdahan
noamsdahan / passrole_actions_and_parameters.csv
Last active November 22, 2023 06:56
A list of IAM actions which require iam:PassRole as of December 2020. Nested parameters are written with dot ('.') notation. Where there are multiple relevant parameters, they are separated by the pipe character ('|'). consult the AWS documentation on special cases - noted with an asterisk (most of them are "array of documents" type parameters).…
IAM Permission Params
amplify:CreateApp iamServiceRoleArn
amplify:UpdateApp iamServiceRoleArn
appconfig:CreateConfigurationProfile RetrievalRoleArn
appconfig:UpdateConfigurationProfile RetrievalRoleArn
appflow:CreateConnectorProfile connectorProfileConfig.connectorProfileProperties.Redshift.roleArn
appflow:UpdateConnectorProfile connectorProfileConfig.connectorProfileProperties.Redshift.roleArn
application-autoscaling:RegisterScalableTarget RoleARN
apprunner:CreateService SourceConfiguration.AuthenticationConfiguration.AccessRoleArn|InstanceConfiguration.InstanceRoleArn
apprunner:UpdateService SourceConfiguration.AuthenticationConfiguration.AccessRoleArn|InstanceConfiguration.InstanceRoleArn