Skip to content

Instantly share code, notes, and snippets.

Matthew Hammer matthewhammer

Block or report user

Report or block matthewhammer

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
matthewhammer / Hammer-writing-preferences.Md
Last active Apr 11, 2018
Matthew Hammer's writing preferences and guidelines (a reference for students and collaborators)
View Hammer-writing-preferences.Md

Matt's Writing Preferences

Below, I am cataloging my writing preferences.

Many of these guidelines simply codify well-established principles for clear, concise technical writing. Some guidelines are specific to me, and others are suggestions that are especially important for reading really wide columns of text, as in this new PACMPL format. :)

matthewhammer /
Last active Mar 5, 2018
Comments on Hazel prototype, somewhat "organized"


Nested contexts


Nested contexts (e.g., nested lets) give rise to nested hole contexts. The current Hazel interface displays paths through this nested structure, with clickable links, which is very cool.

This makes we wonder:

View Time_with_random_points.elm
import Html exposing (Html, div, text)
import Time exposing (Time, second)
import Random exposing (Seed)
main =
{ init = init
, view = view
, update = update
, subscriptions = subscriptions

Curating Hazel Edits

How should we curate edit histories in Hazel so that we can make sense of them, and find patterns and structure in them?

Interacting with terms in Coq and Agda

Let's step back and consider related systems like Cog and Agda (both provide interactive editor services for functional programs, though these have depedent types, unlike Hazel; let's ignore dependent types). Though all of these systems have similar interaction models, Agda's way of doing things is very different from Coq, and both should be different than Hazel:

matthewhammer / DataPipesLang.txt
Created Oct 6, 2017
Data Pipes -- Language Definition
View DataPipesLang.txt
Element types
E ::= Generate(D)
| Consume(D)
| Modify(D1, D2)
| Pair(D1,D2,D3) // D3 is a function of D1 and D2 (its the "product" of the dictionary types)
| Proj(D1,D2,D3) // D2 and D3 are each "projections" of the dictionary type D1
(* Directed graph *)
type graph
val empty : graph
val add_nd : graph -> ndid -> nddat -> (graph, option<nddat>)
val del_nd : graph -> ndid -> (graph, option<nddat>)
val dat_of_nd : graph -> ndid -> optional<nddat>
val adj_of_nd : graph -> ndid -> List<ndid>
val adj_of_nd : graph -> ndid -> (ndid -> α -> α) -> α -> α
type edgeid = (ndid, ndid)

Demand-driven change propagation

If you have a DAG where for each node, you have some local computation (internal to the node) and some external dependencies (other nodes in the DAG that I’ll call the “successors”) and some dependents (other DAG nodes that I’ll call the “predecessors”) then we can consider doing change propagation over this via Adapton’s demand-driven algorithm:

— Dirty the graph (perhaps in parallel) when a reference cell (e.g., input cell) changes, by traversing all dependent (predecessor) edges and marking them dirty. An invariant is that if an edge is dirty, all preceding edges are dirty too, so we can stop dirtying early.

— Clean the graph on demand (of a node in the DAG) by traversing its successor edges that are dirty, until we reach a node that depends directly on a changed input. Re-evaluate that node. If its return value changes, then we need to re-evaluate its predecessors, and so on. Change propagation here is demand-driven, and follows the original order of execution (fo

matthewhammer /
Last active Jul 28, 2018
CS Colloquium, Request Instructions
View git reflog 2
825166bc46 (HEAD -> master) HEAD@{0}: rebase finished: returning to refs/heads/master
825166bc46 (HEAD -> master) HEAD@{1}: rebase: -Z profile-queries: compute 'self' duration; order final summary by 'self' duration, not 'total' duration
763e8ba4b0 HEAD@{2}: rebase: -Z profile-query-and-key, separate from -Z profile-query; query key is string option
40e26f2776 HEAD@{3}: rebase: -Z profile-queries includes dep_graph.with_task uses in output
06be62b0bb HEAD@{4}: rebase: count timed passes in totals; minor CSS stuff
adf3845811 HEAD@{5}: rebase: -Z profile-queries: remove panic when channel is unset
8591d0dc3f HEAD@{6}: rebase: profiling with -Z profile-queries recognizes -Z time-passes
0148826367 HEAD@{7}: rebase: tidy: trailing ws
f723e016d2 HEAD@{8}: rebase: comments from @michaelwoerister
9615098a94 HEAD@{9}: rebase: clean up and fixes, thanks to comments from @kennytm; moved dump logic to profile mod
View git-reflog
4dfdd3d3fc HEAD@{0}: reset: moving to HEAD~10
d105172a10 HEAD@{1}: rebase -i (finish): returning to refs/heads/master
d105172a10 HEAD@{2}: rebase -i (start): checkout refs/remotes/origin/master
d105172a10 HEAD@{3}: rebase: aborting
580ab1ef6f HEAD@{4}: rebase -i (pick): Update release notes for 1.19.0
4545f18562 HEAD@{5}: rebase -i (pick): Allow remote testing remotely when `TEST_DEVICE_ADDR` is set
814f1ea446 HEAD@{6}: rebase -i (pick): Add empty MIR pass for non-lexical lifetimes
d573b9605a HEAD@{7}: rebase -i (pick): Fix checking for missing stability annotations
773ace032f HEAD@{8}: rebase -i (pick): explanatory error on `--print target-spec-json` without unstable options
06f7c0df4c HEAD@{9}: rebase -i (pick): reorder span labels
You can’t perform that action at this time.