Lambda the Ultimate

Hi,

It's a call for kind help; in the form of more relevant pointers I seemingly have missed so far.

I am looking for authoritative reference materials about what people sometimes people refer to as "precise types" (in the programming languages ontology, preferably).

As most people on these forums I suppose, I believe I have grasped a fair enough notion of what we usually mean by static typing (as opposed to the dynamic side of things). The understanding situation on my end is way less comfortable re: "precise types".

I did try to read quite a bit of resources on typing systems and the corresponding, traditionally associated calculi schemes, and their respective, supporting nomenclatures, and I did stumble a couple times upon various phrasings of what the author is alluding to by his/her "precise types", but without really seeing a blindingly obvious common agreement and shared understanding of what is really meant, unambiguously, in a standard fashion by that : "precise types". It still seems to vary significantly from one author to the other.

For one thing, would that be an absolute notion for the qualifying criteria (like, e.g., when opposing a terminating vs. a non-terminating program, or inhabited vs. non-inhabited types, or confluent vs. non-confluent term rewriting systems, etc) or would that be something relative, with type systems offering features to denote "more or less" precise types ?

For another parallel, the signification of the difference (and implications) between the untyped lambda calculus and the many typed lambda calculi flavors one can devise are well understood today. I was expecting the case to be the same when one speaks of (more or less) strongly type systems, offering static type check convenience features but NOT qualifying as being frameworks for precise types, as opposed to the ones which do so. Therefore : if precise types are well understood today, which are the properties that the meta language / logical framework is supposed to have for one to be able to check about the precise types' inhabitation, its helper algorithms, etc, within the type system being defined or scrutinized ?

Thus, does someone know if "precise types" has been given a clearly delimited (small) set of definitions in the process of converging together, or is it still mostly left open to one's context of work (be it on type inference and/or just type checking, or etc) ?

If my question happens to be too much open for today's state of knowledge, I can provide what I (would like to) understand by the usage of the "precise type" phrase, say, in the specific context of static type inference during some compilation/translation process.

Thank you in advance for any relevant pointers.

Hello,
I wanted to discuss my take on a "type class" concept in a dynamically typed language. The language is called Ela (http://elalang.net) and for now it lacks any way to provide a function overloading. The language itself has Haskell/ML style syntax (layout based), is strict by default (lazy by demand), it is also pure and dynamically typed. I was playing with an idea of overloading for quite some time but didn't actually come to a good solution.

So another attempt.

First of all it is quite different from regular type classes as soon as it relies on a dynamic, not static dispatch. Also it is just single dispatch for now (which somewhat logical as soon as all functions are curried).

The preview version (link below) contains three new entities. The first is a 'type' entity that creates a user type:

type user x = User x

This declaration is basically a function (and is first class therefore). The right hand can contain any expression. Here a variant (aka polymorphic variant) tag is used which simply "wraps" a given value. Variant is helpful as soon as it can be used to "unwrap" the value like so:

let (User x) = ...

The second is a 'class' entity, which is defined like so:

class Foo
  foo bar

(This syntax is probably a bit clumsy).
Ela requires that all "class members" are functions, signature is not required as soon as they are untyped. Basically a declaration like the one above creates two global functions 'foo' and 'bar' (classes are mostly ignored by the run-time). These two functions are quite different from regular functions as soon as they are organized as "vocabularies", type-indexed functions.

Having a class and a type one can create an instance of a class for a type like so:

instance Foo user
  where foo (User x) = "Foo:" ++ show x
     et bar (User x) = "Bar:" ++ show x

An instance adds these functions to the previously defined vocabularies.

These vocabularies are basically mutable objects however all instances are always executed before any user code. When implementing an instance it is required to provide an implementation for all functions in a class. It is not possible to override an existing instance (it is not a problem technically however I am not sure that this is a good feature). And of course it is possible to define instances for built-in types (such as int, double, string, list, etc.). "Class functions" also can't be shadowed by other bindings (Ela does support shadowing for regular bindings).

What do you think about such an approach?

There is a preview for this implementation. It only comes with prelude that defines several classes/instances for built-ins and other basic functions (such as composition, application operators, etc.) and REPL. Requires Mono 2.6+/.NET 2.0+, 1MB:
http://elalang.googlecode.com/files/ela-0.11-preview.zip

BTW. There's a short language reference and a side-by-side comparison with Haskell if you're interested:
http://code.google.com/p/elalang/w/list

The following are all midpoints between functional and imperative. What do we lose at each point? At what point does what is lost weigh more heavily than what is gained? Are there other useful points in the value type / reference type spectrum?

Point 1:

In functional code we use immutable data structures. Instead of updating an existing value, we create a new value with the desired updates.

Functional languages often have immutable records and syntax for updating them. For example:

let p = {name="Joe", age=27}
let q = p with {age=28}

With nested records this is not so pretty:

let p = {name="Joe", age=27, address={country="France", street="Rue de la Gare", number=43}}
let q = p with {address = p.address with {number=23}}

This pattern is very common when working with functional data structures. Clojure provide certain functions like update-in and assoc-in to handle these patterns. Oftentimes we don't need the old copy of the data structure anymore in the scope it's in. So we can introduce syntactic sugar for record update:

let p.age = 28

-- is sugar for: --

let p = p with {age=28}

This makes use of variable shadowing. This makes nested record update nice:

let p.address.number = 23

Note that other copies of the record are not affected. It has the same semantics as pass-by-copy structs in C/C++.

We can even drop the let in front of variable bindings:

p.address.number = 23

We can also extend this to custom data types (maps, arrays, sets, domain specific objects, etc.) like Common Lisps places (but functional instead of imperative).

Point 2:

Now on another track. If you want to translate this to a functional language:

if <something>:
  x = <calculation of x if something>
  y = <calculation of y if something>
else:
  x = <calculation of x if not something>
  y = <calculation of y if not something>

Then you have to construct a pair:

(x,y) = if <something>
        then (<calculation of x if something>,
              <calculation of y if something>)
        else (<calculation of x if not something>,
              <calculation of y if not something>)

This style can be less clear and perhaps less efficient. We can adopt dominance based scoping: if a block dominates another block, then the variables defined in the first block are visible in the other block. So we can do:

if <something>
  let x = 2
else
  let x = 3

foo x

And the x will be visible outside the if.

Point 3:

We can extend this principle to loops. Loops in functional languages are often written in recursive style:

let xs = <some list of numbers>
let iter ys n =
  if ys==[]
  then iter (tail ys) (n + head ys)
  else n
let sum = iter xs 0

This is reminiscent of programming with gotos.

We can do structured programming by letting variables shadow each other across loop iterations:

let xs = <some list of numbers>
let sum = 0
for x in xs:
  let sum = sum + x

Point 4:

However, some loops are written with higher order functions:

let xs = 
let sum = 0
foreach xs (fun x -> let sum = sum + x)

It's unclear what the semantics are:

let ref x =
  let val = x
  ((fun () -> val), (fun y -> let val = y))

If we allow this, then we are no longer shadowing previous variables: we can implement full stateful references with it.

Hi,

I was curious to see how JavaScript in my various browser versions is performing lately in the case of both stack-greedy and numeric operations-intensive computations (well, or somehow).

So I made this small big integer-calculator toy language (three keywords only : const, print, and show) providing the usual four operations, the modulus (%), and four builtin functions: the square root (sqrt), the power (pow), the recursive factorial (fact) and a memoizing Fibonacci (fibo).

(the language isn't just a fluent interface hosted by JavaScript; it's parsed by an actual PEG-based parser I made after augmenting Chris Double's jsparse a bit for my needs.)

The results (timings) and differences observed are sometimes interesting.

EDIT:
1. the calculator also knows the first 20 Mersenne primes (consts M1 thru M20); e.g.:

show M20 ;

2. the semicolon is a statement terminator, not a separator
3. no parse error handling at all

https://github.com/ghc-ios/ghc/wiki

A recent article in Wired with quotes from one of our own. Also, this is a good time to bring up Leo et al. publication draft on Socio-PLT along with their project page and a survey to view and take.

From the article:

But no matter how impressive these new languages are, you have to wonder how long it will take them to really catch on — if they do at all. After all, new programming languages arrive all the time. But few ever reach a wide audience.

At Princeton and the University of California at Berkeley, two researchers are trying to shed some light on why some programming languages hit the big time but most others don’t. In what they call a “side project,” Leo Meyerovich and Ari Rabkin have polled tens of thousands of programmers, and they’re combing through over 300,000 computing projects at the popular code repository SourceForge — all in an effort to determine why old languages still reign supreme.

Edit, abstract from paper:

Why do some programming languages fail and others succeed? What does the answer tell us about programming language design, implementation, and principles? To help answer these and other questions, we argue for a sociologically grounded programming language theory: socio-PLT.

Researchers in the social sciences have studied adoption in many contexts. We show how their findings are applicable to programming language design. For example, many programming language features provide benefits that programmers cannot directly or immediately observe and therefore may not find compelling. From clean water to safe sex, the health community has long examined how to surmount similar observability barriers. We use such results from outside
of programming language theory to frame a research agenda that should help us understand the social foundations of languages. Finally, we examine implications of our approach, such as for the design space of language features and the assessment of scientific research into programming languages

The arrow calculus by Sam Lindley, Philip Wadler, & Jeremy Yalloop

We introduce the arrow calculus, a metalanguage for manipulating Hughes's arrows with close relations both to Moggi's metalanguage for monads and to Paterson's arrow notation. Arrows are classically defined by extending lambda calculus with three constructs satisfying nine (somewhat idiosyncratic) laws; in contrast, the arrow calculus adds four constructs satisfying five laws (which fit two well-known patterns). The five laws were previously known to be sound; we show that they are also complete, and hence that the five laws may replace the nine.

I stumbled across this paper while trying to dig a little deeper into Haskell type classes and noticed that no one had mentioned it before. I'm still a novice with the lambda calculus and denotational semantics, but I can appreciate the simplification the paper achieves. It could make correctly implementing the arrow class more intuitive, but do theoretical reductions like this tend to help the compiler do a better job too?

I recently started my own programming language project:

http://code.google.com/p/aha-programming-language/

Please check it out and let me know what you think.

I found this very interesting: What software programming languages were used by the Soviet Union's space program?

The languages DRAGON and Grafit-Floks appear to be graphical. You can see some videos of working with DRAGON.

Tony Hoare wrote his paper "An axiomatic basis for computer programming" in 1969. This led to the so called "Hoare Logic" for software verification.

Up to now all attempts to prove software correct which is written in a language which allows mutable types and references have not yet been satisfactory because of the "framing" or "alias" problem. An object might be reached through different references. Therefore it is necessary to specify not only what a procedure modifies, but also what it leaves unchanged.

Various techniques have been invented to get a hand on this problem: Separation logic, alias calculus, "modify/use" annotations.

In the paper An approach to framing and mutability a new approach is described. It is based on implicit frame contracts. The writer of a procedure just specifies what the procedure is going to modify with the implicit contract that it modifies nothing unspecified. By using a dependency graph of all functions a complete frame contract can be derived from the implicit frame contract.

The paper demonstrates that the derived frame contracts coincide with the ones a user is expecting intuitively.