Lambda the Ultimate

I've just made a public release of AsyncFlows framework 0.1.0 that offers DSL for structured and object-oriented asynchronous programming.

Some differences from competing solutions:

• The framework is implemented in pure Java, there are no compiler extensions used. The same ideas are implementable in any garbage-collected language with reasonable lambdas and where it is possible to implement event queues and promises. The better are lambdas, the better code looks. Kotlin and Groovy versions looks much better than Java version.
• There is no event matching and alomst no explict working with events. Explicit sending and event receiving are considered in the framework as "go to" of asynchronous programming and they should be avoided for the same reasons. Actually framework just uses one type of events: executable action.
• The focus is intra-process coordination. The inter-process communication is considered as subject for libraries, there is no communication model enforced.
• The focus during development are asynchronous operations and their combination using operators. Just like when developing in Java or C the focus are composing blocks, statements, loops, etc. The DSL is inspired by Occam and E language and it provide a set of orthogonal operators (all, seq, any, seq while, etc.).

I would like feedback on DSL struture and on the thesis that explicit event sending to queues or channels is "go to" of asynchronous programming and that it should be avoided if we try to get understandable code.

I'm working on specifying a language for specifying program design, or 'semantic design', called SEDELA. 'Semantic design' is a program design tool inspired by Conal Elliott's 'denotional design' as presented in "Denotational Design: From Meaning to Programs" here -

Denotational Design Talk

Currently, I have specified a rough outline of the syntax and semantics here -

Semantic Design Language

I am thinking very seriously about writing a parser, type-checker, and a Visual Studio Code editing plug-in for SEDELA. But first, I want to get the community's feedback on the current specification as well as the idea in general.

Thank you all once again for any assistance provided in these endeavors!

After couple of years of using a Haskell, I noticed that errors in the code were not decreased (lie, as well as "you will be more productive", "you will write code faster", "code will be smaller" - all of these sentences were a lie), so I thought about it: how to decrease bugs. I know these methods:

• More unit and properties tests (it's available in most languages)
• Free monads - allows to check logic in code which looks like "imperative" without to involve real IO
• Indexed monads - to prevent denied transitions in monad (IO, etc) - IMHO leads to complex less readable code
• Prove tool (Agda, Idris, etc) - seems difficult to use, not sure
• Liquid Haskell - not sure how it helps in real world applications, also not sure will it alive after dependently types introduction in the next GHC versions
• Literate programming - good to decrease logical errors IMHO

The most embarrassing of me circumstance is that, as I understood, most real world errors (not typos and other stupid errors) can not be caught by type system because: 1) they happen in run-time 2) their roots are unexpected behavior of something external 3) often they are logical: some complex business logic is not fully correct but it's difficult to describe it formally even. Also I'm not sure is it possible to qualify anything as some kind of type: types of typical Haskell app are so many, that attempt to use more complex types will lead to something absolutely unreadable and unsupportable.

I think Design by Contract can help to cover some of the errors, but I can not find good DbC framework for Haskell. IMHO it can be something like "predicate under monad", because contract, sure, should be executed with side-effects (I'm interesting to verify some external entities, etc).

In this case all functions like `f :: a -> b -> IO c` become `f :: Ctr a -> Ctr b -> CtrIO c` or something similar. But I'm not sure here, because I need to check not only pre-/post- conditions but also invariants. How they can look in Haskell where you have only spaghetti code of functions? How to code asserting conditions in those monads? I found work of Andres Loh, Markus Degen, but this does not helps me. Most of articles (Peyton-Jones, Andres Loh, etc) look very shallowly, academically or unpractical (on research/experimental level, sure, as all other in Haskell). What do you use to decrease bugs in Haskell code? Also will be very interesting real success stories!

BF Bignum is a program synthesis game: the goal is to synthesize a BF program smaller than a given size that outputs the largest integer possible before halting within a given time limit. A synthesizer's score is the value of the target integer divided the total number of BF operations executed in the search for the target program.

Bignum is much harder than it sounds, and requires synthesizers to learn modular and hierarchical program representations.

• Your BF program must be smaller than a given size, and halt within the given time limit. Time is defined as the number of BF operations executed during the production of the target integer. Synthesizers compete in a size/time class akin to weight classes in martial arts.
• Your BF program must use `.` to produce its output. Your BF program may have any number of outputs; the largest output is the one incorporated in to your synthesizer's score. Note that since there is no input, the instruction `,` is simply ignored.
• Your synthesizer must keep track of the total work done in the search. Work is defined as the number of BF operations executed during the search for the target program, e.g. while computing a candidate program's fitness. Note that two operations done in parallel is still two operations.

  It's not clear that this is the best measure of work, and there may be borderline cases such as static analysis that may or may not be considered execution of a BF program.

• The BF tape contains big integers, not bytes. Your BF program is scored on the largest single integer it outputs; the sequence of integers is not interpreted as a string like in some BF examples.
• You are writing a program that writes a program. You are not writing the bignum program yourself, that's too easy. Of course there are ways to cheat, like including some high fitness program within the source code of your synthesizer. Don't do that.

A synthesizer's score is target / work: the number output by the target program divided by the number of BF operations performed during the search.

I've added this question to StackExchange. I've been wondering if there is any good theory behind making the branch tables when coming from SSA form (which should lose the information that there even existed a switch statement in the source code). Does anybody know any references on that?

I have written a small introduction to untyped lambda calculus.

The article contains nothing new, but it has been written to be easy to understand. The article is not only elementary. It contains all essential results of untyped lambda calculus like the Church Rosser theorem and some undecidability theorems.

I have tried to use graphic notations to make the content more digestible and closer to intuition. I am especially proud of the proof of the Church Rosser theorem which (hopefully) is more understandable in this article than in many other presentations I have read so far.

Joseph A. Goguen, Higher Order Functions Considered Unnecessary for Higher Order Programming (1987).

It is often claimed that the essence of functional programming is the use of functions as values, i.e., of higher order functions, and many interesting examples have been given showing the power of this approach. Unfortunately, the logic of higher order functions is difficult, and in particular, higher order unication is undecidable. Moreover (and closely related), higher order expressions are notoriously difficult for humans to read and write correctly. However, this paper shows that typical higher order programming examples can be captured with just first order functions, by the systematic use of parameterized modules, in a style that we call parameterized programming. This has the advantages that correctness proofs can be done entirely within first order logic, and that interpreters and compilers can be simpler and more efficient. Moreover, it is natural to impose semantic requirements on modules, and hence on functions. A more subtle point is that higher order logic does not always mix well with subsorts, which can nonetheless be very useful in functional programming by supporting the clean and rigorous treatment of partially dened functions, exceptions, overloading, multiple representation, and coercion. Although higher order logic cannot always be avoided in specification and verification, it should be avoided wherever possible, for the same reasons as in programming. This paper contains several examples, including one in hardware verification. An appendix shows how to extend standard equational logic with quantification over functions, and justifies a perhaps surprising technique for proving such equations using only ground term reduction.

This (old paper) proposes an interesting approach for formulating functional programs. But can this truly subsume all uses of higher order functions? I don't see the paper address how the uses of higher order functions in general can be replaced (not that I have a counterexample in mind).

Anyone familiar with the OBJ language? Do other languages share this notion of 'modules', 'theories'?

Are there any prior examples of programming languages that expose the program processing lifecycle as a value or syntax element?

By lifecycle, I mean steps like the below which many languages follow (though not necessarily in order):

1. lex: turn source files into tokens
2. parse: parse tokens into trees
3. gather: find more sources with external inputs
4. link: resolve internal & external references
5. macros: execute meta-programs and macros
6. verify: check types, contracts, etc.
7. compile: produce a form ready for loading
8. run: load into a process that may be exposed to untrusted inputs

Does anyone have pointers to designs of languages that allow parts of the program to run at many of these stages *and* explicitly represent the lifecycle stage as a value or syntax element?

I'm aware of reified time in hardware description languages like Verilog and in event loop concurrent languages like JavaScript and E, but that's not what I'm after.

Background

I work in computer security engineering and run into arguments like "we can either ship code with dynamic languages that is hard to reason about the security properties of, or not ship in time."

I'm experimenting with ways to enable features like the below but without the exposure to security vulnerabilities or difficulty in bringing sound static analysis to bear that often follows:

• dynamic loading,
• embedded DSLs,
• dynamic code generation & eval,
• dynamic linking,
• dynamic type declaration and subtype relationships & partial type declarations,
• powerful reflective APIs

I was hoping that by allowing a high level of dynamism before untrusted inputs reach the system I could satisfy most of the use cases that motivate "greater dynamism -> greater developer productivity" while still producing static systems that are less prone to unintended changes in behavior when exposed to crafted inputs.

I was also hoping, by not having a single macros-run-now stage before runtime, to allow use cases that are difficult with hygienic macros while still allowing a module to limit how many assumptions about the language another module might break by reasoning about how early in the lifecycle it imports external modules.

The end goal would be to inform language design committees that maintain widely used languages.

cheers,
mike

The lambda calculus is not upward confluent, counterexamples being known for a long time. Now, what about the interaction calculus? Specifically, I am looking for configurations c₁ and c₂ that have the same normal form with no such c that c →* c₁ and c →* c₂.

Update: a necessary and sufficient condition for strong upward confluence discussed in arXiv:1806.07275v3 which also shows that the condition is not necessary for upward confluence by showing upward confluence for the interaction system of the linear lambda calculus.

Hello,thought I’d share a new DSL by endgame life querying security logs : https://www.endgame.com/blog/technical-blog/introducing-event-query-language

It is meant to help reason about security events. Best illustrated in this example:

What files were created by non-system users, first ran as a non-system process, and later ran as a system-level process within an hour?

sequence with maxspan=1h
[file where event_subtype_full=="file_create_event" and user_name!="SYSTEM"] by
file_path
[process where user_name!="SYSTEM"] by process_path
[process where user_name=="SYSTEM"] by process_path

While I could easily see how this can be expressed as SQL instead and perhaps backends do do that, I think it helps analyst to think about logic rather than data.

I think that there is a lot of improvement that can be had in. languages that help reason about (time) series and it’s a welcome addition to the DSL family.