Skip to content

Instantly share code, notes, and snippets.

View pelotom's full-sized avatar

Tom Crockett pelotom

252 followers · 11 following
  • Los Angeles, CA
View GitHub Profile
@pelotom
pelotom / relayXSpy.js
Created March 11, 2021 22:56
Add this to the relayx market page to see what orders are being added and removed
(() => {
if (__relayXSpy) {
__relayXSpy.disconnect();
}
var __relayXSpy = new MutationObserver(records => {
records.forEach(({ addedNodes, removedNodes }) => {
for (const added of addedNodes) {
console.log('added', printNode(added));
}
@pelotom
pelotom / axis-title-overrun.spec.json
Last active February 19, 2019 05:20
Example of a chart with axis labels overrunning axis title
{
"$schema": "https://vega.github.io/schema/vega/v4.json",
"width": 300,
"height": 240,
"padding": 5,
"config": {
"axis": {
"labelLimit": 500
}
@pelotom
pelotom / explode-points.json
Last active July 23, 2018 23:41
Experiment in making points explode away from one another on hover
{
"$schema": "https://vega.github.io/schema/vega/v4.json",
"width": 700,
"height": 100,
"padding": {"left": 5, "right": 5, "top": 0, "bottom": 20},
"autosize": "none",
"signals": [
{ "name": "cx", "update": "width / 2" },
{ "name": "cy", "update": "height / 2" },
@pelotom
pelotom / index.html
Created February 19, 2017 23:01
<!DOCTYPE html>
<html>
<head>
<title>Elea Crockett Portfolio</title>
<meta http-equiv="refresh" content="0; url=https://eleacrockett.github.io/portfolio/" />
</head>
<body>
</body>
</html>
@pelotom
pelotom / existential.ts
Last active May 18, 2022 10:08
Encoding of existential types in TypeScript
type StackOps<S, A> = {
init(): S
push(s: S, x: A): void
pop(s: S): A
size(s: S): number
}
type Stack<A> = <R>(go: <S>(ops: StackOps<S, A>) => R) => R
const arrayStack = <A>(): Stack<A> =>
@pelotom
pelotom / tagged-template-dsl-example.js
Last active December 30, 2020 11:18
const λ = ({raw}, ...subs) => {
const expr = raw
.reduce((prev, next, n) => prev + `(___subs[${n - 1}])` + next)
.replace(/#(\d+)/g, (_, n) => `(___args[${n}])`)
const evaluate = new Function('___subs', '___args', `return (${expr});`)
return (...args) => evaluate(subs, args)
}
@pelotom
pelotom / curry.idr
Last active August 29, 2015 14:09
A dependent curry and uncurry.
curry : {A : Type}
-> {B : A -> Type}
-> {C : Sigma A B -> Type}
-> ((p : Sigma A B) -> C p)
-> (x : A) -> (y : B x) -> C (x ** y)
curry f x y = f (x ** y)
-- Dependent uncurry is just the induction principle for sigma types
uncurry : {A : Type}
-> {B : A -> Type}
@pelotom
pelotom / 1-monoid-sigma.idr
Last active January 18, 2021 09:40
A comparison of implementing a Monoid type using 1) Idris Sigma types, 2) an Idris dependent record, 3) an Agda dependent record
BinOp : (A : Type) -> Type
BinOp A = A -> A -> A
parameters ((*) : BinOp a)
IsAssociative : Type
IsAssociative = (x, y, z : _) -> x * (y * z) = (x * y) * z
IsLeftIdentity : a -> Type
IsLeftIdentity e = (x : _) -> e * x = x
@pelotom
pelotom / DecideParity.idr
Last active August 29, 2015 14:07
Idris code for the problem posed in Joseph Abrahamson's type theory talk http://jspha.com/posts/papers_we_love_BOS_2/
-- Axioms
rec_N :
(P : Nat -> Type) ->
(ind : (n : Nat) -> P n -> P (S n)) ->
(base : P Z) ->
(m : Nat) ->
P m
Even : (n : Nat) -> Type
Odd : (n : Nat) -> Type
zeroIsEven : Even Z
@pelotom
pelotom / multDistOverPlus.idr
Created September 15, 2014 00:43
Multiplication distributes over addition
-- Informal proof:
--==============================================================
-- S a * (b + c)
--= b + c + a * (b + c) -- definition of *
--= b + c + (a * b) + (a * c) -- induction hypothesis
--= b + (a * b) + c + (a * c) -- associativity / commutativity
--= S a * b + S a * c -- definition of *
-- With all associativity and commutativity manipulations:
--==============================================================