Showing posts with label Dynamic and Static Typing. Show all posts
Showing posts with label Dynamic and Static Typing. Show all posts

14.10.19

The Next 7000 Programming Languages


The Next 7000 Programming Languages, by Chatley, Donaldson, and Mycroft, appears in a book marking 10,000 volumes of LNCS. Though they riff on Landin's title, the authors consider something quite different: Darwinian evolution in the context of programming languages. I've long thought we need a theory of the economics of programming languages, to explain why the most popular language is not always that one might consider best suited to a task. But, until now, it's not been clear to me what such a theory might consist of, other than the observation that network effects apply to programming languages. This paper points in the direction of a theory of programming languages as a whole, drawing on evolutionary theory and with a potential grounding in empirical measures, such as scraping Github to measure which languages are more or less popular.

It is useful here to distinguish between the success of a species of plant (or a programming language) and that of a gene (or programming language concept). For example, while pure functional languages such as Haskell have been successful in certain programming niches the idea (gene) of passing side-effect-free functions to map, reduce, and similar operators for data processing, has recently been acquired by many mainstream programming languages and systems; we later ascribe this partly to the emergence of multi-core processors.

This last example highlights perhaps the most pervasive form of competition for niches (and for languages, or plants, to evolve in response): climate change. Ecologically, an area becoming warmer or drier might enable previously non-competitive species to get a foothold. Similarly, even though a given programming task has not changed, we can see changes in available hardware and infrastructure as a form of climate change—what might be a great language for solving a programming problem on a single-core processor may be much less suitable for multi-core processors or data-centre solutions.

Amusingly, other factors which encourage language adoption (e.g. libraries, tools, etc.) have a plant analogy as symbiotes—porting (or creating) a wide variety of libraries for a language enhances its prospects.

1.12.15

Static vs. Dynamic Languages: A Literature Review

A thorough study by Dan Luu. From the introduction:
The summary of the summary is that most studies find very small effects, if any. However, the studies probably don’t cover contexts you’re actually interested in. If you want the gory details, here’s each study, with its abstract, and a short blurb about the study.
And from the conclusion:
Other than cherry picking studies to confirm a long-held position, the most common response I’ve heard to these sorts of studies is that the effect isn’t quantifiable by a controlled experiment. However, I’ve yet to hear a specific reason that doesn’t also apply to any other field that empirically measures human behavior. Compared to a lot of those fields, it’s easy to run controlled experiments or do empirical studies. It’s true that controlled studies only tell you something about a very limited set of circumstances, but the fix to that isn’t to dismiss them, but to fund more studies. It’s also true that it’s tough to determine causation from ex-post empirical studies, but the solution isn’t to ignore the data, but to do more sophisticated analysis. For example, econometric methods are often able to make a case for causation with data that’s messier than the data we’ve looked at here.

The next most common response is that their viewpoint is still valid because their specific language or use case isn’t covered. Maybe, but if the strongest statement you can make for your position is that there’s no empirical evidence against the position, that’s not much of a position.
Thanks for the effort you put into this epic study, Dan! Spotted via Lambda the Ultimate.

21.7.14

Meditations on Using Haskell

Bitemyapp - Meditations on Using Haskell explains why and how those in the trenches use Haskell, by quoting from conversations on an IRC channel.

E

So when i found haskell i slingshotted off through dependent and substructural types. Assuming that if a little was good a lot was better. Made it half way through TaPL and found pure type systems, coq, etc.
I think the power to weight ratio isn’t there. I find that Haskell gives amazingly expressive types that have amazingpower for the amount of code you tie up in them and that are very resistant to refactoring.
If i write agda and refactor I scrap and rewrite everything. If i write haskell, and get my tricky logic bits right?
I can refactor it, split things up into classes, play all the squishy software engineering games to get a nice API I want. And in the end if it still compiles I can trust I didn’t screw up the refactoring with a very high degree of assurance.

C

Admittedly I’m not playing at the level E is, but this was my experience. I can make sweeping changes to my API, get all the bugs caught by the type system, and still have minimal code impact.

B

That is what I was getting at with the tweet about not using dynamically typed langs because I need to be able to prototype quickly and get rapid feedback.
I think a lot of my friends thought i was just being trollish. Even just being able to see what would have to change if you changed your design slightly and being able to back it out quickly…

21.3.14

Facebook announces Hack

Julian Verlauget and Alok Menghrajani of Facebook have announced Hack, a gradually-typed variant of PHP. Hack is released open-source, features support for generic types and higher-order functions, and and compiles to HHVM. The core team for Hack features a number of the usual suspects, including Bryan O'Sullivan and Erik Meijer. Meanwhile, Simon Marlow and others at Facebook are pressing ahead with Haxl, a Haskell-based project.
However, Hack adds additional features beyond static type checking, including Collections, lambda expressions, and run-time enforcement of return types and parameter types.
Collections provide a clean, type-safe alternative to PHP arrays. We designed them specifically to work well with static typing and generics. The Collections API offers many classic higher-order functions such as map() and filter() to facilitate functional programming styles.
Lambda expressions give a concise syntax for creating closures. While PHP has closures, it requires the programmer to explicitly name the variables they need to use from enclosing scopes. With Hack's lambda expressions, we automatically infer these uses, saving you needless work. Lambda expressions make it more convenient to take full advantage of the Collections API.
Run-time enforcement of return types and parameter types (including scalar types like int and string) provides safety beyond what can be checked statically while type annotations are being gradually added to a codebase. Run-time enforcement helps programmers detect and diagnose certain kinds of problems more easily, and it helps HHVM's JIT produce more efficient code by making it safe to trust type annotations for optimization purposes.
Spotted by Shayan Najd.

10.3.14

Microsoft Research PhD Scholarship: TypeScript, The Next Generation

We are recruiting one PhD student to work on design and implementation of programming languages. The post is on the project TypeScript, The Next Generation, and is funded by a Microsoft Research PhD Scholarship.

There is increasing interest in integrating dynamically and statically typed programming languages, as witnessed in industry by the development of the languages TypeScript and Dart, and in academia by the development of the theories of gradual types, hybrid types, and the blame calculus. The purpose of our project is to bring the academic and industrial developments together, applying theory to improve practice.

Our project focusses on JavaScript, an ECMA standard, and its typed variant TypeScript, an open-source project sponsored by Microsoft. JavaScript plays a central role in web-based applications and the new Windows 8 framework, and TypeScript is seeing rapid takeup, with over 150 JavaScript libraries now provided with TypeScript declarations. Our project has two parts, one aimed at immediate short-term application, and one aimed at fundamental long-term research.
  • TypeScript TNG The short-term goal is to build a tool, TypeScript: The Next Generation (or TypeScript TNG for short), that generates wrapper code from TypeScript import declarations to detect and pinpoint type errors. A wrapper will accept any JavaScript value as input, and either raise an error or return a value guaranteed to satisfy the invariant associated with the corresponding type. In particular, wrappers for generic types will assure surprisingly strong guarantees, known as “theorems for free”. Our hypothesis is that TypeScript TNG will aid debugging and increase reliablility of TypeScript and JavaScript code.
  • A wide-spectrum type system. The long-term goal is to extend the foundations of the blame calculus to support a wide-spectrum of type systems, ranging from dynamic types (as in JavaScript or Racket) through generic types (as in F# or Haskell) to dependent types (as in F* or Coq). Our hypothesis is that a wide-spectrum type system will increase the utility of dependent types, by allowing dynamic checks to be used as a fallback when static validation is problematic.
The workplan is likely to be too ambitious for a single PhD studentship. Which aspects are carried out will depend on which seem the most promising as our work develops, and on the abilities and desires of the student.

The successful candidate will join the ABCD team, carrying out a research programme investigating sesion types and web programming. The project is jointly supervised by Andrew Gordon of Microsoft Research Cambridge and the University of Edinburgh.

You should possess an undergraduate degree in a relevant area, or being nearing completion of same, or have comparable experience. You should have evidence of ability to undertake research and communicate well. You should have a background in programming languages, including type systems, and programming and software engineering skills.

It is desirable for candidates to also have one or more of the following: a combination of theoretical and practical skills; experience of JavaScript or web programming; knowledge of dependent type theory; or training in empirical measurement of programming tasks. We especially welcome applications from women and minorities.

We seek applicants at an international level of excellence. The School of Informatics at Edinburgh is among the strongest in the world, and Edinburgh is known as a cultural centre providing a high quality of life.

The successful candidate will receive a studentship covering tuition and subsistence. Students from the UK or EU are preferred. Consult the University of Edinburgh website for details of how to apply.

If you are interested, please send an outline of your qualifications to: Prof. Philip Wadler (wadler@inf.ed.ac.uk).