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
615 followers · 141 following
View GitHub Profile
@copumpkin
copumpkin / FinVector-cons.agda
Last active October 14, 2020 05:12
module FinVector-cons (T : Set) where
data Nat : Set where
zero : Nat
suc : Nat → Nat
data Fin : Nat → Set where
zero : ∀ {n} → Fin (suc n)
suc : ∀ {n} → Fin n → Fin (suc n)
@copumpkin
copumpkin / aws-shell
Created March 28, 2019 19:58
AWS Shell
#!/usr/bin/env bash
PIPE=$(mktemp -u)
mkfifo $PIPE
# TODO: parse properly
ROLE="$1"
ID="$2"
./metadata-service.py $PIPE $ROLE $ID &
@copumpkin
copumpkin / extract.py
Last active May 2, 2022 11:15 — forked from 0xdabbad00/extract.py
Parse IAM info from https://docs.aws.amazon.com/IAM/latest/UserGuide/list_awsservicecatalog.html
#!/usr/bin/env python
from os import listdir
from os.path import isfile, join
import re
import json
from bs4 import BeautifulSoup
"""
@copumpkin
copumpkin / SelectiveSigma.hs
Last active August 17, 2019 11:47
{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, DataKinds, PolyKinds, TypeOperators, ScopedTypeVariables #-}
-- Lots of ways you can phrase this, but this works for me
-- For folks who haven't seen it before, this is "the essence of the sum type" and sigma stands for sum.
-- You see it far more often in dependent types than elsewhere because it becomes a lot more pleasant to
-- work with there, but it's doable in other contexts too. Think of the first parameter to the data
-- constructor as a generalized "tag" as we talk about in "tagged union", and the second parameter is the
-- "payload". It turns out that you can represent any simple sum type you could write in Haskell this way
-- by using a finite and enumerable `f`, but things can get more unusual when `f` isn't either. In such
-- cases, it's often easier to think of this as the essence of existential types.
@copumpkin
copumpkin / Instances.hs
Created July 17, 2015 22:21
Map parametrized by "named Ord instances"
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
module Instances where
data Map o k v = Map
{ mapOrder :: k -> k -> Ordering
, mapImpl :: () -- You'd stick your actual map implementation as another field here and hide the constructor
}
data ForgottenMap k v = forall o. ForgottenMap (Map o k v)
@copumpkin
copumpkin / Ack.agda
Created June 2, 2015 01:41
Ackermann
module Ack where
-- http://en.wikipedia.org/wiki/Ackermann_function#Definition_and_properties
data Nat : Set where
zero : Nat
suc : Nat → Nat
{-# BUILTIN NATURAL Nat #-}
@copumpkin
copumpkin / FingerStar.agda
Created April 9, 2015 01:17
module FingerStar where
open import Level using (_⊔_)
open import Algebra
open import Data.Empty
open import Data.Product hiding (map)
open import Data.Nat hiding (compare; _⊔_)
open import Data.Nat.Properties
open import Data.Vec renaming (map to mapVec) hiding ([_])
@copumpkin
copumpkin / Relations.agda
Created July 9, 2014 04:15
Relations form a semiring!
-- See also https://gist.github.com/copumpkin/2636229
module Relations where
open import Level
open import Function
open import Algebra
open import Data.Empty
open import Data.Sum as Sum
open import Data.Product as Prod
open import Relation.Binary
@copumpkin
copumpkin / classifiers
Created May 3, 2014 21:51
Chinese classifiers and the words they classify, built from CC-CEDICT and Max Bolingbroke's cjk Haskell package
[箇 个 [ge4] /variant of 個|个[ge4]/,個 个 [ge4] /individual/this/that/size/classifier for people or objects in general/]
鼻子 鼻子 [bi2 zi5] /nose/CL:個|个[ge4],隻|只[zhi1]/
鼓舞 鼓舞 [gu3 wu3] /heartening (news)/boost (morale)/CL:個|个[ge4]/
黨員 党员 [dang3 yuan2] /political party member/CL:名[ming2],位[wei4],個|个[ge4]/
黨 党 [dang3] /party/association/club/society/CL:個|个[ge4]/
黑板 黑板 [hei1 ban3] /blackboard/CL:塊|块[kuai4],個|个[ge4]/
黃鱔 黄鳝 [huang2 shan4] /swamp eel/finless eel/CL:個|个[ge4],條|条[tiao2]/
鬼 鬼 [gui3] /ghost/sly/crafty/CL:個|个[ge4]/
高麗菜 高丽菜 [gao1 li4 cai4] /cabbage/CL:顆|颗[ke1],個|个[ge4]/
高度 高度 [gao1 du4] /height/altitude/elevation/high degree/highly/CL:個|个[ge4]/
@copumpkin
copumpkin / Resource.hs
Last active August 29, 2015 13:58
Can you break my shitty linear resource monad transformer? Looking for people to find ways that it's unsafe.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE RebindableSyntax #-}
module Resource where