Tom Crockett pelotom
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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
/ relayXSpy.js
Created
March 11, 2021 22:56
Add this to the relayx market page to see what orders are being added and removed
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (() => { | |
| if (__relayXSpy) { | |
| __relayXSpy.disconnect(); | |
| } | |
| var __relayXSpy = new MutationObserver(records => { | |
| records.forEach(({ addedNodes, removedNodes }) => { | |
| for (const added of addedNodes) { | |
| console.log('added', printNode(added)); | |
| } |
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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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
/ tagged-template-dsl-example.js
Last active
December 30, 2020 11:18
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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
/ axis-title-overrun.spec.json
Last active
February 19, 2019 05:20
Example of a chart with axis labels overrunning axis title
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "$schema": "https://vega.github.io/schema/vega/v4.json", | |
| "width": 300, | |
| "height": 240, | |
| "padding": 5, | |
| "config": { | |
| "axis": { | |
| "labelLimit": 500 | |
| } |
pelotom
/ explode-points.json
Last active
July 23, 2018 23:41
Experiment in making points explode away from one another on hover
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "$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
/ index.html
Created
February 19, 2017 23:01
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <!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
/ unapply trickiness
Created
April 27, 2013 08:27
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| // Here's the problem I was having: | |
| scala> val unapply = implicitly[Unapply[Applicative, List[Int]]] | |
| unapply: scalaz.Unapply[scalaz.Applicative,List[Int]] = scalaz.Unapply$$anon$14@5a977cac | |
| scala> implicitly[Unapply[Applicative, unapply.M[unapply.A]]] | |
| <console>:15: error: Unable to unapply type `unapply.M[unapply.A]` into a type constructor of kind `M[_]` that is classified by the type class `scalaz.Applicative` | |
| 1) Check that the type class is defined by compiling `implicitly[scalaz.Applicative[<type constructor>]]`. | |
| 2) Review the implicits in object Unapply, which only cover common type 'shapes' | |
| (implicit not found: scalaz.Unapply[scalaz.Applicative, unapply.M[unapply.A]]) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| public static abstract class List<a> { | |
| private static final class $Nil<a> extends List<a> { | |
| private $Nil() { | |
| } | |
| public <M> M match(final M $ifNil, final $F<a, $F<List<a>, M>> $ifCons) { | |
| return $ifNil; | |
| } | |
| } |
pelotom
/ Brouwer-communication
Last active
December 20, 2015 07:38
Excerpts from van Stigt's "Brouwer's Intuitionist Programme"
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Brouwer's philosophy of language starts from the conviction that direct | |
| communication between human brings is impossible. His chapter on "Language" | |
| in "Life, Art and Mysticism" starts as follows: "From Life in the Mind | |
| follows the impossibility of communicating directly with others... Never | |
| has anyone been able to communicate directly with others soul-to-soul." | |
| The privacy of mind and thought and and the hypothetical existence of minds | |
| in other human beings, who are no more than the Subject's mind-creations, | |
| "things in the exterior world of the Subject" rule out "any exchange of | |
| thought". |
NewerOlder