Themes
I have two overarching questions:
- How can we reason about notations/interfaces/editors? So that:
- We can construct correct interfaces
- We can distill what we are trying to say into more direct representations
- We can explore the consequences of what we are trying to say more directly
- How can we construct more direct analogies for computation?
All the questions below are quite rough. They all need to be made more precise and concrete. I have a lot of notes elsewhere on most of these questions, but just wanted to get a relatively complete and maybe over-general list of the questions I have been thinking about. Please reach out on twitter or mastodon or leave a comment here if you have feedback or want to talk about any of these questions!
Questions
Computer Science
- Can we visualize and explore a universe of “computational paths”?
- What do equal functions with different implementations look like in this universe?
- What are the primitives? How do they compose? Can we visualize in such a way that Universal functions are easy to see?
- What does composition look like?
- What does computational complexity look like? Distance?
- Computational complexity is relative. i.e. having access to a solution to a NP-complete problem lets you solve other NP-complete problems. What does this look like combinatorally?
- How can we focus the visualization and/or computational model so that it is not too complex?
- What would Inheritance look like? Equipment?
- How does this relate to types?
- Transporting functions across isomorphisms/equivalences
- $f = g[b_0, b_1,... b_n]$ (re-implementing basic functions from another type in the type of f, then composing) (how can I properly express this??)
- $f = i \circ g \circ i^{-1}$ (mapping from the type of f to another type where g is defined and back)
http://jdh.hamkins.org/the-hierarchy-of-logical-expressivity/
Examples of function dependence
https://martin-ueding.de/posts/graph-of-game-of-life-states/
I want a “toy” model that captures some of these phenomena in a simple visual way.
- Can we translate between local and global descriptions of functions?
- e.g. instances of a function that run on each node of a tree and “pass the baton” between each other v.s. a function that runs on the entire tree itself.
looping is a global operation on a list while recursion on a list is local in this sense?
- What can we do with constructed bidirectional functions?
B = T | F
0 = on | off
J = 1 | -1
b1 : B <-> J
b1 T :=: 1
b1 F :=: -1
o1: 0 <-> J
o1 on :=: b1 1
o1 off :=: b1 -1
- What can we do with user-defined type-eliminators / destructuring?
- How can we implement system of nudge-able bidirectional functions.
- Can we create a table of pull/push in/out style function composition?
- relationships to continuations, promises, observables,…?
Notation
- How can we reason about notation so that we can construct notations with properties we want?
- How can we decouple syntax and semantics?
- We want notation with properties that are homomorphic to the semantics.
- Can we design notations for arithmetic and algebra that are more directly homomorphic to their semantics? e.g. the subtraction symbol -sucks. e.g. for set of objects that are defined as equivalence classes of drawing in R2, commutative operations can be defined to be operations that are just juxtaposition of drawings where positioning of juxtaposition doesn’t matter.
https://www.youtube.com/watch?v=oUaOucZRlmE
A part of my notebook on Polytope.