Lambda the Ultimate

Hello,

I am looking for papers and a particular paper I used to have on covariance and contravariance.

The paper I used to have many years ago probably about 2006 or 2007 when I originally started looking into type theory and did not realize its relevance had many inference rules for covariance and contravariance using plus and minus symbols within the inference rules.

I am now researching this area and am interested in any papers on this topic.

Many thanks in advance,

Aaron Gray

Recently, while re-reading through the Haskell Typeclassopedia I thought it would be a good exercise to map the structure of software design-patterns to the concepts found in the Haskell type class library and in functional programming in general.

By searching the web I found some blog entries studying specific patterns, but I did not come across any comprehensive study. As it seemed that nobody did this kind of work yet I found it worthy to spend some time on it and write down all my findings on the subject.

I think this kind of exposition could be helpful if you are either:

- a programmer with an OO background who wants to get a better grip on how to implement complexer designs in functional programming
- a functional programmer who wants to get a deeper intuition for type classes.

I have set this up as a GitHub project with full sourcecode for all examples:

The Patternopedia

POLA Would Have Prevented the Event-Stream Incident by Kate Sills

The JavaScript world was rocked this week by news that the popular npm package event-stream included malicious code that attempted to steal the private keys of certain Bitcoin users.

Since the attack was discovered, both the JavaScript community and the cryptocurrency community have been passionately debating how to prevent such an attack. At Agoric, we think this attack was entirely preventable, and the answer is POLA, the Principle of Least Authority.

This npm / event-stream debacle is the perfect teaching moment for POLA (Principle of Least Authority), and for the need to support least authority for JavaScript libraries. My talk Securing EcmaScript, presentation to Node Security explained many of these issues prior to this particular incident.

For LtU, my best explanation of POLA is Verify What? Navigating the Attack Surface given to the "Formal Methods Meets JavaScript" workshop at Imperial College.

https://youtu.be/rp_Eild1aq8

Monads are passé, apparently.

Previously mentioned on ltu rather a long time ago http://lambda-the-ultimate.org/node/5151

I’m looking at type theory from point of view of the general-purpose programming language evolution, and I’ve found something that does not look nice.

There is stage when function pointers like ones in C were introduced to the languages. Differently from lambdas they are stateless and they could be only evaluated using their explicit arguments and using only constants (or global state) and by calling other stateless functions. Their type will be designated as:

T ⇨ A

Now let’s take usual lambdas, their type will be designated as:

T → A

The relationship between these two types is the following:

A → B = ∃ T (T ⨉ (T ⨉ A ⇨ B))
apply:  (A → B) ⨉ A ⇨ B = ? ((t, f), a), f(t, a) // unpacking existential type here
curry: ((A ⨉ B) → C) ⇨ (A → B → C) = ?(t, f) ((t, f), (?((t1, f1),  a1) ((t1, f1, a1),  (?((t2, f2, a2), b2)  f2(t2, (a2, b2))))))

Such definition is needed to support currying and to capture implicit environment, and it reflects what is actually happens in the code. Every function from T ⇨ A could be trivially converted to T → A, however stateless functions have different set operations supported. Particularly, currying is not supported. So, it is not subclass, but a separate entity type.

This existential type captures difference between structured programming paradigm and object-oriented or functional programming paradigms. So, theoretically, when we would try to study paradigms, we would also need to make this distinction.

I’m interested if there are some research papers that describe this distinction. The discussion in the TaPL book is somewhat unsatisfying because explicit existential types are defined using implicit existential types. Theoretically, the type theory should start from stateless functions to reflect evolution path rather than in reverse direction. Such point of view might be also useful for the compiler transformation reasoning, so there might be papers on such equivalence in that area too.

Golly, how did I never hear of this before?

Flix is a declarative language for specifying and solving fixed-point computations on lattices, such as static program analyses. The syntax and semantics of Flix are inspired by Datalog, but extended to support user-defined lattices and monotone functions. Flix is open-source and available on GitHub.

Static analyzers implemented in general-purpose languages, such as C++ or Java, can be difficult to understand and maintain. A more elegant approach is to express the mutual dependencies of a fixed-point computation in a declarative manner. Thus, there is interest in using a declarative language such as Datalog to implement pointer analyses.

However, Datalog does not support lattices or functions, which limits its expressivity. While it is sometimes possible to work around these limitations, it can be slow and cumbersome. Furthermore, most Datalog implementations have poor integration with existing tools.

Flix allows users to define their own lattices and functions. Rules over relations and lattices are expressed in a logic language with Datalog-like syntax, while functions are written in a pure functional language with Scala-like syntax. The functional language, while small, supports algebraic data types, sets, and pattern matching. Flix also supports interop with JVM languages.

Flix is implemented in Scala, with a standard front-end for parsing, weeding, resolving, and typechecking. The back-end has two components, a solver for the logic language and an interpreter for the functional language. As an initial step to improve performance, we have implemented a bytecode generator to replace the interpreter.

I thought I'd let you all know about a video lecture I gave on Scheme continuations, and how they can be used to generate all sorts of control structures. Enjoy!

Continuations: The Swiss Army Knife of Flow Control

My old half-baked idea/dream of a cranky day job programmer who doesn't really know what he's talking about:

• Convert everything in to CPS.
• Each function call is a new continuation.
• Have a top level 'event loop' that runs the next continuation one at a time.
• The runner checks the signature of the next function vs. a lookup table for hooks to run before and/or after the invocation.

This gives super powers like:

• AoP join points at every function. In languages that are more expression than statement oriented, more pure fp style, then that means there's a lot of opportunity for join points.
• Logging is more flexible, at any join point, dynamically adding/removing/tweaking at runtime.
• Ability to run prod & test versions of any function side by side and compare behaviour.

Code would still be interacted with by developers in original format. Since e.g. hypothetically anything can be converted from imperative to monadic pure fp style then e.g. Java could be set up this way. The UX for adding hooks would be nice and all at a high level, looking like source code, not some internal runtime CPS hell.

Shift/reset allow convenient expression of monadic computations, as a kind of generalized, functional version of do-notation. From the beginning of that link:

Continuations represent the rest of the computation. Manipulation of continuations is a powerful tool to realize complex control flow of programs without spoiling the overall structure of programs. It is a generalization of exception handling, but is far more expressive.

The obvious question is whether there is an analogous construct for comonads. Given that there is a codo-notation I believe there is.

In a concatenative language, shift/reset can be written as:

[F] shift K reset = [K] F reset

The F block observes the future of the computation (delimited by the nearest reset) and may select a new one.

I believe the comonadic dual is:

coreset E [F] coshift = coreset [E] F

The F block observes the past of the computation (delimited by the nearest coreset) and may select a new one.

This leads to a combined operator:

{ E [F] shift K } = { [E] [K] F }.

The F block observes the future and past of the computation (delimited by the nearest braces) and may select new ones. This is first class (co)control flow.

I want to say something like "the dual of continuations is environments", as "environment" is an existing concept that seems conceptually close to "store". Note that on this page, someone posts functions analogous to shift/reset for "codensity" or "store".

          redex
        ---------
    { E [F] shift K }
      ^           ^
  environment continuation

I believe this notation allows the convenient expression of arrows (and monads and comonads) in the same way shift/reset allows expression of monads. Arrows allow decoration of both inputs and outputs, as opposed to only inputs for comonads and only outputs for monads.

This makes sense to me but I'm not totally sure since there's not much information on comonads/codo notation and such. I'd appreciate any comments.

EDIT: I think the correct format is actually

{ E [F] shift K } = [{ E }] [{ K }] F

Seen on Twitter.