Instead of using call-by-value (CBV), I often use Call-by-push-value (CBPV) in my core calculi, and many people ask me "why?".
Most reasons relate to the "fine-grained" typed structure that it introduces, and the ability of this structure to describe "low-level" concerns, like the difference between partial and full function application (of curried,
| type ICPTs = record { | |
| e8s : nat64; | |
| }; | |
| type Duration = record { | |
| secs: nat64; | |
| nanos: nat32; | |
| }; | |
| type TimeStamp = record { |
| // Recursion via "manual back-patching" | |
| // | |
| // What? | |
| // MyClass is defined recursively with myFunc, which refer to each other. | |
| // | |
| // How? | |
| // The myClass method uses a variable for mutable storage (myClass_) to | |
| // determine if the initialization has occured yet or not. | |
| class Test() { |
Archive:
⇨ Fall 2017 Calendar
People
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 makes we wonder:
| import Html exposing (Html, div, text) | |
| import Time exposing (Time, second) | |
| import Random exposing (Seed) | |
| main = | |
| Html.program | |
| { init = init | |
| , view = view | |
| , update = update | |
| , subscriptions = subscriptions |
How should we curate edit histories in Hazel so that we can make sense of them, and find patterns and structure in them?
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:
| Types | |
| ----------- | |
| 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) |
