Lambda the Ultimate

I've recently been looking at a notion of interfaces for BitC. The language already has type classes in the style of Haskell, with all of the pros and cons of these. The deeper my dive into interfaces, the more confused I became about the difference between interfaces and type classes. This either means that I'm hopelessly confused or that I've stumbled into something useful. I'm sure the LtU audience can explain my confusion. :-)

BitC has object-style methods in a syntactic sense, but no virtual methods or inheritance. In such a language, object methods are sugar. We also have a notion of interfaces, currently called "capsules". A capsule provides existential encapsulation of an underlying object combined with a known set of methods. In contrast to Java-style interfaces, a capsule type has an explicitly invocable constructor. This means that a capsule can have non-default instantiations for a given underlying type T. Capsule constructor arguments corresponding to method initializers are constrained to be compile-time evaluable. This has the consequence that every capsule "method table" is a compile-time constant in the same way that every type class instance method table is a compile-time constant.

Capsules may have either static of conventional methods. A static is method does not receive or require a reference to the encapsulated object.

The lifetime of a capsule instance is guaranteed not to exceed the lifetime of the object (if any) that it encapsulates.

Q: How is a capsule type consisting exclusively of static methods different from a type class, if at all?

(Obviously of possible interest for some language implementors)

By Jämes Ménétrey (aka "ZenLulz") :

MemorySharp

MemorySharp is a C# based memory editing library targeting Windows applications, offering various functions to extract and inject data and codes into remote processes to allow interoperability.

The goal of this library is to provide a safe, powerful and easy to use API, keeping the remote process as clean as possible. This library is said Out-of-Process, in other words it does not need to be injected within the target process. Only your application loads MemorySharp, ensuring that only the requested operations are executed in the opened process. For the moment, the library only supports 32-bit development.

Home page:

http://binarysharp.com/products/memorysharp/

Also on GitHub: https://github.com/ZenLulz/MemorySharp

and on NuGet: http://www.nuget.org/packages/MemorySharp/

Fasm.NET

A managed wrapper to use the FASM compiler from .NET applications.

This library is written in C++/CLI and embeds FASM compiler as a linkable Microsoft COFF object. As FASM compiler is built in 32-bit, the managed assembly can only be used within a 32-bit development.

The branches match with the current versions of FASM compiler as published on the official website.

Home page:

http://binarysharp.com/products/fasmnet/

Also on GitHub: https://github.com/ZenLulz/Fasm.NET

and on NuGet: http://www.nuget.org/packages/Fasm.NET/

Licensing

Both librairies come with the MIT license:

* MemorySharp, since 9/14/2013 (Announcement)

* Fasm.NET, as of v2.0.0

Excerpt from MemorySharp's feature list :

Process interactions

* Check if the process is debugged
* Gather information of the process
* Interact with the PEB (Process Environment Block)

Memory interactions

* Allocate and free a chunk of memory
* Change the protection of allocated regions
* Get an absolute/relative address from a pointer
* Query the memory allocated
* Read and write primitive and complex data types

Module interactions

* Enumerate all modules loaded
* Find functions inside a module
* Get the main module
* Inject and eject modules

Thread interactions

* Create and terminate threads
* Get the exit code of terminated threads
* Get the main thread
* Get the segments addresses
* Get threads by identifier
* Interact with the TEB (Thread Environment Block)
* Join threads
* Manage the context of threads
* Query the state of threads
* Suspend and resume threads

Window interactions

* Enumerate the windows of the process
* Enumerate the child windows of the process
* Enumerate the child windows of another window
* ...

Assembly interactions

* Assemble mnemonics
* Embed FASM compiler (Fasm.NET)
* Execute remote codes (such as functions) with/without parameter(s) synchronously and asynchronously
* Inject mnemonics
* Support several calling conventions

(... and more)

Fasm.NET's feature list :

* Assemble mnemonics on the fly
* Assemble a file
* Assemble multiple files
* Create a instance of the class to assemble your mnemonics code with ease
* Throw managed and detailed exceptions when compilation errors occur
* Customize the memory size and the number of pass
* Get the version of the FASM compiler

...

(A few FASM links)

• FASM - flat assembler : http://www.flatassembler.net/ (home page)
• "FASM (flat assembler)" (on Wikipedia)
• "What is FASM - A brief introduction to the Flat Assembler" (on winasm.net)

P.S.

Happy new year 2014, everybody, "by the way" :)

And a random fact, as of 01/01/2014:

both the CLR and C# are still in their teenage, for just a couple more years to come... ;)

Cheers,

I'm looking at how different statically typed languages tackle the problem of letting you define types and define interface implementations for those types.

For example, to define an implementation of interface I for type T, Java uses interface methods, Haskell uses typeclasses, Scala uses implicits.

The disadvantage of the Java approach when compared with Haskell/Scala:

• You need a value of type T to call the method.
• equals() isn't symmetric.
• Must implement interface for T in the same module as T. This is probably not much of a problem for equality/ordering/hashing, but can be problematic for interfaces that aren't part of the core library.

Haskell approach vs Scala approach:

• Haskell only allows one interface implementation per type, whereas Scala lets the programmer specify the implementation explicitly at the constraint site, if necessary. I can see arguments for both.
• Scala's implicits allow more simple overriding. I don't see why you'd want to override equality/ordering, but maybe redefining hashing could be useful?

What do you think is the "right" way to do this? Given my limited knowledge right now, I think I'd go with something Scala-like and maybe make some modifications. For example, I think the "only one implementation per type" restriction of Haskell might be useful.

Is there a good survey of the different approaches?

So I've been working on a new language for a while and the topic of how to implement closures came up. I have seen closures usually implemented on the heap or with some malloc region of memory. This seems suboptimal so I thought of it some more and came up with the idea of using type unions to store local variables. This way closures could be passed around on the stack normally.

Obviously this has downsides if you hold too many local variables or few large ones. Since this has probably been done before, I would like to ask the community what their experiences have been with alternative closure implementations.

Also to note, specialization of functions is an option that could help reign in the size of the closure struct.

Coq developpers recently put together a survey of their tool usage, which will hopefully inform future evolutions. From Matthieu Sozeau's announcement:

On behalf of the Coq developers, I’d like to invite everyone to respond to a survey on their usage of Coq, its programming and proving environment, development model, shortcomings and future directions. This survey aims at gathering important information about Coq's users and uses. The results will be used to better understand users' needs, and help decide in which direction Coq’s development should go. It is really important for us to get as many answers as possible before * January 15th 2014 *. We are also taking this occasion to collaboratively build a bibliography of Coq-related papers. The survey’s results will be synthesized, anonymized and made publicly available in february.

The estimated burden time for this survey is around 30 minutes. The survey is available online at:

https://sondages.inria.fr/index.php/276926/lang-en

This survey was mainly prepared by Thomas Braibant, assisted by Enrico Tassi, thanks to them for giving us all an occasion to take a step back and reflect on Coq’s future.

Microsoft's Joe Duffy and team have been (quietly) working on a new programming language, based on C# (for productivity, safety), but leveraging C++ features (for performance). I think it's fair to say - and agree with Joe - that a nirvana for a modern general purpose language would be one that satisfies high productivity (ease of use, intuitive, high level) AND guaranteed (type)safety AND high execution performance. As Joe outlines in his blog post (not video!):

At a high level, I classify the language features into six primary categories:

1) Lifetime understanding. C++ has RAII, deterministic destruction, and efficient allocation of objects. C# and Java both coax developers into relying too heavily on the GC heap, and offers only “loose” support for deterministic destruction via IDisposable. Part of what my team does is regularly convert C# programs to this new language, and it’s not uncommon for us to encounter 30-50% time spent in GC. For servers, this kills throughput; for clients, it degrades the experience, by injecting latency into the interaction. We’ve stolen a page from C++ — in areas like rvalue references, move semantics, destruction, references / borrowing — and yet retained the necessary elements of safety, and merged them with ideas from functional languages. This allows us to aggressively stack allocate objects, deterministically destruct, and more.


2) Side-effects understanding. This is the evolution of what we published in OOPSLA 2012, giving you elements of C++ const (but again with safety), along with first class immutability and isolation.


3) Async programming at scale. The community has been ’round and ’round on this one, namely whether to use continuation-passing or lightweight blocking coroutines. This includes C# but also pretty much every other language on the planet. The key innovation here is a composable type-system that is agnostic to the execution model, and can map efficiently to either one. It would be arrogant to claim we’ve got the one right way to expose this stuff, but having experience with many other approaches, I love where we landed.


4) Type-safe systems programming. It’s commonly claimed that with type-safety comes an inherent loss of performance. It is true that bounds checking is non-negotiable, and that we prefer overflow checking by default. It’s surprising what a good optimizing compiler can do here, versus JIT compiling. (And one only needs to casually audit some recent security bulletins to see why these features have merit.) Other areas include allowing you to do more without allocating. Like having lambda-based APIs that can be called with zero allocations (rather than the usual two: one for the delegate, one for the display). And being able to easily carve out sub-arrays and sub-strings without allocating.


5) Modern error model. This is another one that the community disagrees about. We have picked what I believe to be the sweet spot: contracts everywhere (preconditions, postconditions, invariants, assertions, etc), fail-fast as the default policy, exceptions for the rare dynamic failure (parsing, I/O, etc), and typed exceptions only when you absolutely need rich exceptions. All integrated into the type system in a 1st class way, so that you get all the proper subtyping behavior necessary to make it safe and sound.


6) Modern frameworks. This is a catch-all bucket that covers things like async LINQ, improved enumerator support that competes with C++ iterators in performance and doesn’t demand double-interface dispatch to extract elements, etc. To be entirely honest, this is the area we have the biggest list of “designed but not yet implemented features”, spanning things like void-as-a-1st-class-type, non-null types, traits, 1st class effect typing, and more. I expect us to have a few of these in our mid-2014 checkpoint, but not all of them.

What do you think?

John has written a long and promising blog post on abstractive power.

Another four decades of experience (since Standish's post-mortem on the extensible languages movement) suggests that all programming languages have their own envelopes of reachable extensions. However, some languages have much bigger, or smaller, envelopes than others. What factors determine the size, and shape, of the envelope? What, in particular, can a programming language designer do to maximize this envelope, and what are the implications of doing so?

As a useful metaphor, I call the breadth of a language's envelope its radius of abstraction. Why "abstraction"? Well, consider how the languages in this envelope are reached. Starting from the base language, you incrementally modify the language by using facilities provided within the language. That is, the new (extended) language is drawn out from the old (base) language, in which the new language had been latently present.

[..]

The Smoothness Conjecture [defined earlier in the post] is a neat expression of a design priority shared by a number of programming language designers; but, looking at programming language designs over the decades, clearly many designers either don't share the priority, or don't agree on how to pursue it.

What, though, if we could develop a mathematical framework for studying the abstractive power of programming languages — a theory of abstraction. One might then have an objective basis for discussing design principles such as the Smoothness Conjecture, that to date have always been largely a matter of taste.

I'll admit I haven't read it yet, but I'm very happy to see it and hope some of you may be as well -- I even dare to suspect that recent mentions of this topic here on LtU may have been one of the motivations for the large effort of John to write and release this document.

Now for a hefty amount of reading, and then some programming language discussion!

Implementing non-intrusive runtime polymorphic objects with value-semantics, and multiple-undo in 20 minutes.

I found this talk by Sean Parent to be very informative (and it's 24 minutes long). What do you think?

For a few years now, I've been working on a textbook introducing the Coq proof assistant. It's been available freely online, and I'd like to announce now the availability of a print version from MIT Press. The site I've linked to includes links to order the book online.

Quick context on why LtUers might be interested in Coq: it supports machine checking of mathematical proofs, including in program verification and PL metatheory, some of the most popular applications of proof assistant technology.

Quick context on what distinguishes this book from other Coq resources: it focuses on the engineering techniques to develop large formal developments effectively. It turns out that there are some reusable lessons on how to write formal proofs so that they tend to continue to work even when theorem statements change over the courses of projects.

I'm grateful to MIT Press for agreeing to this experiment where I may continue distributing free versions of the book online.

A new completely rewritten and improved version of my previous Going Against the Flow paper. Abstract:

This paper introduces a novel type system that can infer an object's composition of traits (mixin-style classes) according to its usage in a program. Such "trait inference" is achieved with two new ideas. First, through a polyvariant treatment of assignments (a := b) and implied field sub-assignments, assignment can usefully encode trait extensions, method calls, overriding, and so on. Second, rather than unify term types or solve inequality constraints via intersection, we instead propagate trait requirements "backward" to assignees, ensuring that trait requirements are compatible only for terms used in the program. We show how this system is feasible without type annotations while supporting mutability, sub-typing, and parametricity.

The main innovation in this work is a treatment of fields and assignment to support it. We have found that assignment between a term's fields is parametric with respect to the assignments of that term! Intuitive but semantically tricky. Soundness proof of this treatment is included in the paper, along with a feasible (but unproved) way of implementing it. Anyways, once that's done, we can model the entire type system in terms of assignments and fields, which I don't think has been done before.