You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
Internet computer ledger utility supporting 2 step transfer (separate sign and send)
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
Matthew Hammer's writing preferences and guidelines (a reference for students and collaborators)
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. :)
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 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
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:
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
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 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