Latest revision as of 09:44, 5 May 2024

Annotated lambda diagrams (ALDs) are a proposed interactive programming interface.
This page presents some mockups about what functionalities could be implemented and how they could be used.
For a basic gist about ALDs see main page: Annotated lambda diagrams

Drag and drop interaction with program fragments and typed holes

Moving program fragments through programs and linking them up via typed hole connection ports

Dragging the program fragment f12 (upper right) into an other yet incomplete function f14 where the types (T1 and T2) match up and connections snap in place. Only unsaturated type-holes display their type to keep visual noise low.

Dragging the function f12 (upper right) into an other yet incomplete function f14 where the types (T1 and T2) match up and connections snap in place.
Imagine the whole thing interactive and animated. As soon as f12 is dragged into the box of f14 it'd get displayed in the same simplified way ad f23 already is. This is not shown.
Dragging f12 around in the box of f14 will move stuff around to make space accordingly.
Wrong connections can be enforced this will make explicit typed holes of bridge type (bridge holes). Not shown.

• Grey cross upper right means this function is expanded and its definition is shown
• Grey shuriken like star upper right means this function is collapsed and its definition is hidden
• Note how f12 (once dropped into f14) gets added to the collected semi-implicit dependencies of f14 (light grey annootations)

Dragging "bridge-holes" or "gap-holes" through still ambiguous sections of the code

See related page: Typed holes

Dragging "bridge holes" through sections of code that are still ambiguous in type. That would be an interesting exotic feature to have. It's kind of complementary to dragging functions or program fragments around.

Visual cues employing human image reconition skills – identicons and arity cues

Visual cues employing human image recognition capability. This might seem a bit playful and silly, but employed correctly this might give a notable increase in enjoyment and productivity when telling computers what to do. Note that only unsaturated holes (the construction sites of coding) would get displayed highly "visually verbosely" be default.

Zooming user interface (ZUI)

From scaled down in place preview to zooming user interface

In place code preview in annotated lambda diagrams

This mockup was put together in order to illustrate how annotated lambda diagrams would allow for
an (adjustably) scaled-down in-place preview of functions on which the currently looked at function depends on.

Specifically this random example code (the "replicate"-function) takes a value and a natural number and
returns a list of copies of that value with the length of that natural number.

In place preview:
Check out the "replicate"-function (grey border).
Looking closely into the expanded version (second from left) you can see:

• the scaled down "in place preview" of the "take"-function (blue border) and
• the scaled down "in place preview" of the "repeat"-function (red border)

This is not yet an evaluating substitution!
Note that (despite this looking like a substitution) this is only just a yet-unevaluated in-place-preview.
This is important. This is very different to "conventional" box and wire graphical programming.
(matching the structure of the plain lambda diagrams)

Actual honest-to-goodness evaluation amounts to short-circuiting:

• vertical-abstraction-lines (always on the right) with
• vertical application-lines (always on the left).

That entails:

• all abstraction lines of the substituted in function that got saturated just vanish (note that partial application is allowed)
• what was formally supplied via the lines now gone is now supplied by the abstraction lines of the callee
• former guts of the now substituted-in function are now arbitrarily complexly intertwined into the calling function

Note that with true substituting evaluation there is a loss decomposition.
Creating complex patterns from simple rules is the point of programming after all.

Is this true?: Classical box-and-wire graphical programming cannot make a distinction between in-place-preview and actual substitution?
If so we might be onto something here.

Annotated lambda diagrams with zooming user interface as a window into the entire control flow multiverse

The desire here is to implement in place previews (with adjustable relative scaling factor)
to annotated lambda diagrams in such a way that:

• in place previews can be arbitrarily deeply nested.
• one can zoom-travel though all of this via a global zoom going across all nesting levels (at least global in a viewport window)

The representation would allow for visualization of the activity of the garbare collector.

Peering into the entirety of the control flow multiverse while it's running live. The lines highlighted in dark blue mark the control flow path that is active at the current moment of execution time (possibly paused). A bright cyan background marks the active case-of-branches. – The "demo" function performs constructive corecursion with dataconstructors. The "showBinFancily" function performs deconstructive recursion with the case of construct. (TODO: Investigate avoiding recursive definitions alltogether. See Book: "The Little Typer")

Some of the massive practical challenges in implementing an ALD-ZUI:
Typical graphic GUI libraries are totally

• not built for zooming user interface (ZUI) like zoomability and
• not built for displaying very very big numbers of elements.
  

Even with special purpose solutions it is difficult ...

A naive redraw of the whole screen for every frame (as often done in computer games)
is is not a viable option (for anything beyond an interactive mockup prototype).
Instead usage of off-screen graphic buffers is essential – partially updated not fully redrawn
(this is e.g. not supported by the webgl wrapper-libraries of the elm language as of 2021 – learned the hard way).
Redrawing only the changing graphic details on mutable graphics-buffers
can easily lead to graphic glitch like artifacts from bugs if not done
with proper fool-proof usually performance expensive abstractions.
Further adding to the difficulty here.

The design choice for off-screen partially updated graphic-buffers becomes necessary due to the following challenges and requirements:

• With tree like visual nesting the amount of elements displayed on screen can grow very fast to seriously problematic numbers.
  
• In a live coding mode (that should be supported) a lot of the displayed elements may need to be refreshed at a high frame rate.
  
• As soon as the computer idles the CPU/GPU load should drop to near zero because this is not a computer game where permanent high load is acceptable.
  

Furthermore:
Regular rescaling of the zoom level during intense zoom-navigation is essential. This is:

• to prevent very quickly running out of the number-range that float-values can represent without rounding errors
• to make dropping off (or heuristic pre-loading) of parts of the visualization easier that are way too small or way too big to see.

Notice the interesting duality of:

• the type-constructors used to construct a value in the "demo" function – constructive corecursion
• the case-of type-destructors used to deconstruct that value in the "showBinFancily" function – deconstructive recursion – handleCases

Maybe interesting side-note: There is definition by (not necessarily terminating) recursion present here.
There are ways to avoid "definition by recursion" alltogether.
All that is needed is a termination case and a provable overall monotonous approach towards that termination case.
Well, these can be obfuscating and brain bending.
This is related to:

• "dependent type theory"
• total programming – provably terminating (necessarily turing incomplete subset)
• the book: "The Little Typer" (official website for the book) (the pie language on guithub - a minimum viable dependently typed language)
  (docs on implementing such a language – by David Thrane Christiansen – implementation language is Racket a scheme/lisp dialect)
• the dependently typed programming language "idris"

"Inverse tabs" for browsing the whole codebase graph rather than only the local code dependency tree

The obvious code navigation options include:

• Tracing down to the codebase into the dependencies (the functions that the currently observed function depends on) and going back up that same path again.
• Following the codebase along the some execution trace.

This is not enough!!
We need "inverse tabs".
We want also be able to quickly jump to functions that answer the question:
What other functions do call this function too that we currently look at?
By switching over to a different "inverse tab" one keeps looking at the same function in the tab but
the whole surrounding (visually represented) context gets switched out.
So when zooming out by scrolling one goes a different way in the codebase.

Essentially this gives one access to the whole directed graph of the codebase not just to a local dependency tree.

Inverse tabs are indicated in the mockup graphic about "peering into the control flow multiverse" at the lower left.
To make it easier to reference to a yellow killroy face has been added.
(wiki-TODO: Make a new mockup focused on showing the idea of inverse tabs better.)

The several types of zooming

See: Annotated lambda diagram#The several types of zooming

Mockups regarding Conal Elliotts work

Tangible values (TVs)

See main page: Tangible values (Conal Elliott)

(wiki-TODO: Add a mockup for combining ALDs with TVs as result value annotations. This one is VERY important!!)

The desire:
Totally obliterating the GUI-vs-commandline rift by combining tangible-value-GUIs with a spectrum of code projections all the way to textual.
Annotated lambda diagrams sitting smack in the middle between graphical and textual.

Priority #1:

• Investigate Conal Elliots work about "tangible values" in the context of ALDs

Tangible values may give a GUI that is pretty much indistinguishable from the GUI's we have today.
But with all windows and graphical elements "secretly" being tangible values in the background.
Assuming the inverse operation of tangible-value-fusion (let's call it "fission" here) is implemented too (which very much should be done IMO)
then the tangible values (as GUI elements) already come with some progressive disclosure.

Progressive disclosure by "fission" (complementary to presented "fusion") can only expose things that do have already implemented graphical representations though.
So an idea here (beyond what Conal Elliott presented in his demo "Eros") is to allow for progressive disclosure of the code
that is associated with the tangible

• not just via fission but
• also via annotated lambda diagrams. (Which come with their own mean of progressive disclosure that is ZUI zooming)
  
• (and also via textual code projections if so desired)

Just about any combination goes of code/data visualization is thinkable.
Only TV-GUI-element, ALD + TV-GUI-element, only ALD, ..., only textual code
When both are shown (ALD + TV-GUI-element) then having relative scaling between the two adjustable (keeping their combined size constant) should be useful.

• This would work like a seesaw making one bigger makes the other smaller (and eventually vanish)
• This is different to the overall global zoom scaling of ALDs that is a main mean to browse codebases.
• This is different to adjusting the relative zoom scale of the local in place previews.

Related notes:

• Default values (for looking at a slice of a stateless tangible value) are living outside the stateless realm.
  They can be stored on disk as additional necessarily stateful data.
  
• Code flowing around holes on the data level rather than the type level (See: Hazel) might be very useful.

Compiling to categories

Priority #2:

• Investigate Conal Elliots work "Compiling to Categories" (which is abstracting with closed cartesian categories CCCs over lambda calculus)
  But that done from within ALDs (which essentially are lambda calculus)
  Out of this reason this likely won't yield a nice representation. Maybe? Still interesting to investigate.
  (wiki-TODO: Continue work on ALD mockups related to "compiling to categories".)

Example usage context #1 (relevant for this wikis context):
Compiling the exact same code to:

• rendered 3D-previews of physical objects
• actual instructions for manufacturing systems for making these physical objects

Example usage context #2:
Compiling to specialized hardware like FPGAs (field programmable gate arrays) and other modern novel HW processing architectures.
This could maybe help in eventually extending progressive disclosure down to the deepest bits of hardware.
Before that this new technology needs to come out of its "proprietary cradle walls" first that are to a good part still standing as of date of writing (2021).

An astounding number of further example usage contexts are given by the work itself.

Related: Curry-Howard-Lambeck isomorphism

Beautiful differentiation

Priority #3:

• Investigate Conal Elliots work "Beautiful differentiation" – Will just turn into a library I guess

In the context of this wiki and in the context of manufacturing in general this is useful e.g. for
3D modelling with surfaces defined by implicit functions (algebraic varieties) and the more restricted class of signed distance functions (SDFs).

• First derivation of a scalar field defined by an implicit function (gradients) can be used to find vertices on surfaces via root finding algorithms (Newton, Regula Falsi, ...)
• Second derivative of scalar fields (Hesse matrices) give curvature that can e.g. be used to determine how densely the local triangulation mesh needs to be to sufficiently accurately approximate the target structure.

For more see: Constructive solid geometry

Overloading the meaning of the lines – (applicative funtors, monads, ...)

In essence these structures are tools for "program abstraction" that is for code reuse and deduplication.

Monads

There are many monad tutorials out there because it's a hard to explain concept ...

• One challenge in explanation is that it is such a general concept,
  with concrete application cases being quite dissimilar and thus
  building an intuition taking quite a number of examples to work through.
• Another challenge in explanation is that the two main existing textual notations (binding notation and do notation) both have major shortcomings.

Annotated lambda diagrams diagrams might at least greatly help in alleviating the latter challenge.
Here is an example that shows the usage of the Maybe monad.
The maybe monad was chosen here for it is one of the most simple ones.

Mockup: Usage of the Maybe monad visualized with annotated lambda diagrams.

One downside of monads is that they do not compose well.
Composition leads to monad-transformer-stacks with ...

• ... an arbitrary stacking order -- representing a form of incidental complexity
• ... a stacking hierarchy -- leading to nested "lift" operation to access into the monad-transformer-stack
• ... accumulating stack depth

There is an alternative approach serving a similar functionality called "algebraic effects".
Algeabraic effects do not form stacks like monads do. But it's not just a typeclass as monad is.

Applicative functors

(wiki-TODO: Add the mock-up showing usage of an applicative functor in lambda diagrams.)

Arrows

...

(wiki-TODO: Make mockups still that are not yet made)

• Continuous transformation from the abstract syntax tree (as a most direct code projection) to ALDs as code projection
  Now added on the page: annotated lambda diagram ☺

The following two (typeclasses and algebraic effects) turned out to be challenging.
E.g. in case of operator-overloading / and-hoc-polymorphism the design goal of
visual continuity of traversing ALD-code-circuits seems hampered by
the necessity of diving through some lookup code that should be
smart and efficient rather than naive and elegant.

• Representation of "algrebraic effects (or abilities)" in ALDs (maybe not a nice match – unfortunately ...)
• Investigate representation of typeclasses in ALDs (typeclasses similar to what is present in the programming language haskell)

Investigate porting some of Jonathan Edwards work in his subtext demo series to ALDs: ( https://vimeo.com/jonathoda )

• No Ifs, Ands, or Buts 2016 – Uncovering the Simplicity of Conditionals – Jonathan Edwards
  – MIT Computer Science and Artificial Intelligence Lab
  – (pdf) – (video)
• Reifying programming 2017
• Direct Programming 2018

Mockups regarding maybe not so practical stuff

• Church encoding in lambda diagrams – more efficient binary encoding
• Encoding of list and enums (product types and sum types respectively) – there's a certain interesting asymmetry in minimal encoding
  (wiki-TODO: dig that out and link it here)
• What about progressive exposure all the way down to the bits and bytes of an open source processor with extensionally equivalent naive inefficient implementations
  both serving as documentation but still switchable in – Related: Multiplication circuits (and their surprising richness), Ternary logic, p-adic numnbers, ...
  

Warning! you are moving into more speculative areas.

• Relation of typed holes to the void type, absurd function and the like – "void" being sort of on the top of the infinite pecking order: type, kind (type of type), sort (type of type of type), ... not inside of any provably terminating "toy formalism"

Notes on conventional/classical "graphical programming" code projections

Conventional graphical programming typically follows the scheme of data-wires and function-boxes.
Thee are approaches that reverse that function-wires and data-boxes but that seems just bad in a different way.

Note: Assuming a function B (represented as a box) has an input that accept a function as an input (that is the function is a so called "higher order function")
then the wire transmitting some other input function to that input is still a "data wire"!
In contrast a function wire is a wire that represent a data-transformation itself.
(Most graphical programming tools do not even allow for using data wires as channels for transmission of functions.)

Annotated lambda diagrams (only a "semi graphical" code projection)
have inherently integrated the capability of overloading the meaning of the graphical lines that connect to other lines.
E.g. monoids, applicative functors, monads, ...
What may seem like boxes are just annotations of the lines.
That is removing the boxes the code still works.
That is not the case for classical graphical programming.

This can be done in classical box and wire representation too.
But it is not inherent. That is not something what one would implement in an naive approach.
And thus it is has rarely (never?) been done.
One concrete case of a programming language attempting that is the (multi representational) language called enso (formerly luna).

What is truly unique to ALDs -- the semi graphical code projection of ALDs is that
Abstractions and applications remain separate in the graphical representations.
(TODO: think about why this might be the killer advantage over box and wire representation)

Related

• Annotated lambda diagram – Lambda diagram – Lambda calculus
• Software
• Projectional editors
• User interfaces for gem-gum on-chip nanofactories
• Typed holes