Lambda the Ultimate

Having learned C++ I thought exceptions was a new, cool thing, simply the new Right way of doing it. I just never could get it right. I thought the problem was that I had been doing C for far too many years, until I stumbled across

Exceptions considered harmful

I then realized I've always done fatal error handling by killing the currently executing thread (or process when not using an RTOS), and normal handling by return value. For most part it worked well. There was one thing I had been missing: Automatic resource deallocation, where focus on automatic is more on "you can't forget" rather than "compiler will do it for you", though I wouldn't mind if the latter could be done safely.

I then stumbled on

Flow manifesto

Using Flow concepts as basis, would it be possible to get same help with generic resource deallocation as Flow offers for memory deallocations?

During the development of a language which allows formal verification I have experimented a lot with proof formats. First I have started with a proof language with tactics similar to Isabelle/HOL and Coq. But then I realized that such proofs are fairly difficult to read. In order to understand a proof one often writes down the state of the proof engine at intermediate positions of the tactics. Then I have introduced proof procedures stimulated by some examples in the dafny language.

Up to now I think that tactics are not appropriate to write down and document proofs. In the posts Boolean lattices, Predicates as sets and Complete lattices and closure systems I have used a proof format which I think is good to write down and document proofs.

Any opinions, remarks etc. are welcome.

I've found that I struggle to read & say math when I encounter it in computer science (papers, proofs, etc.). I find this makes it hard to process them even if I know what the symbols mean I may not know how to "say" them. I found Logitext (http://logitext.mit.edu/logitext.fcgi/main) to be helpful, but even then I found that with some of the symbols (turnstile) I was uncertain if that's how it's pronounced that way or somehow else.

What books, online resources, tutorials, reference sheets, etc. are helpful for learning & being able to read math - specifically math used in computer science & programming language design?

Thanks.

I am the creator of the Opa programming language. As we target web developers, we get an enormous amount of feedback from developers who often don't know much about functional programming and strong static typing.

Here is a tool we have built to please the "dynamic crowd": opa-watch.

Any thoughts?

I've noticed a lot of noise recently about getting rid of mandatory semicolons in mainstream imperative languages because...well...we can! I remember when this move was made in Scala, it was a bit painful with corner cases and error messages, but most of the community was happier with it. But I thought we lost something, let's look at the good and bad of semicolons:

Bad:

• That semicolons can be inferred deterministically means that they are redundant.
• Visual verbosity and clutter.
• extra (keyboard) typing.
• Anachronistic.

Good:

• Redundancy enhances error detection (and robust IDE tooling in general).
• Redundancy enhances readability.
• They aren't really that hard to type.
• Inference that depends on parsing probably goes a bit too far (Scala) in that its not always obvious to human readers where semicolons are inferred.

Did I miss anything?

True or False?

Programmers should not be required or allowed to specify any choice of algorithm or representation when a clearly better choice having equivalent results can be found by analysis, profiling, and consultation of a large knowledge base.

Compilers should for example treat any code describing a bubblesort, once detected, as a call to a better sorting algorithm. If this requires extensive analysis to figure out exactly how to map the bubblesort onto the better sort, then damnit that analysis ought to be done!

The minimal "compiling" tests used by most compilers are only enough to find the most simple and obvious optimizations and bugs. Working through the whole knowledge base may take weeks of time on all of your company's thousand servers, so it should be a background task that runs continuously.

Automated agents distributed with the IDE should participate in a distributed network to gather and share knowledge about code equivalents and optimizations as they are discovered. If any pattern of code existing in the local codebase is proven semantically equivalent to some class of more efficient implementations, by any agent anywhere in the world, then the news ought to come to the local agent via the network, so that next time, and every subsequent time, that local code gets compiled, the compiler will know that it should be compiled as though it were one of those more efficient implementations.

Likewise, any analysis technique which can, statically or dynamically, detect unambiguous bugs (such as 'malloc' being called while a call frame for a destructor is on the stack in C++, or detecting race conditions in threaded code, or detecting a side effecting function used in an "assert", etc) should, once discovered, be distributed over the network and, on receipt and periodically thereafter, run against the local codebase. These tests ought to be running continuously, in round-robin style, in the background whenever any workstation has the IDE or the headless agent running, and the work ought to be shared out to all IDE's and agents accessing the same codebase so as to minimize the total time to complete testing of the whole codebase in its current version.

These tests and optimizations should remain in the knowledgebase until a later test subsumes their functionality, or until expired by local policy or size limits on the local knowledgebase. If expiry becomes common, then they should be redistributed at intervals.

The Daily WTF should be triaged as a source of outrageous examples of wrong or wasteful programming practices, and 'proper' implementations for each correct but horribly-inefficient or wasteful example found there ought to be part of the knowledge base. Likewise, anything there which is clearly a bug no matter what the circumstances, ought to be part of the knowledge base and if static tests can be devised to detect similar bugs, they ought to be.

Is this an extreme position? I think it is, but I also believe it has merit. Why not do this?

Ray

I'm working on a Haskell library implementing the ideas in George Hart's book Multidimensional Analysis: Algebras and Systems for Science and Engineering. In essence explains the way that physical dimensions propagate through matrix equations when different locations in a single matrix may not share the same physical dimension, which happens all the time in a bunch of useful engineering/optimization/signal-processing applications.

This is all well and good, and the dimensional library is a great jumping-off point that handles all of the type-level arithmetic.

My question/puzzle is in several parts, so I'll start with a motivating example.

If you look at the dimensional library, or most any approach to static typing of physical dimensions (or units, whether to track dimensions or units is a separate battle which I'm not exploring today), it works by representing dimensioned quantities using a phantom type that encodes their dimensions. When you do this in a library you end up with Double and Quantity DOne Double (to use dimensional's names as an example) being two separate types. This is annoying because they are logically equivalent. Appearances of the former basically mean "I am a function that uses a Double and I was written before the language learned about the existence of dimensions", and this doesn't seem to be a useful property to encode in the type system. So you end up with *~ one and /~ one at a lot of interfaces between "dimensionally aware" and "dimensionally naive" libraries; dimensional even encodes _1 :: (Num a) => Quantity DOne a and a bunch of similar shorthands for expressing commonly used dimensionally aware, but dimensionless, constants.

There are two solutions to this untidyness:

The first is introducing a system for user-defined coercions between types. The drawback is that inferring where to put such coercions is difficult, complicates/clutters the principle type of pretty much every polymorphic function, and doesn't mix well with a lot of other type system features that are desirable. In summary, it's good if your language already has it, but adding it to your language to solve this problem opens a large can of worms.

The second is to simply declare that all numbers have a dimension, it's just coincidence that that dimension is often 1. In Haskell-speak, you move all the types like Int, Integer, Float, Rational etc from kind * into a new kind, say Integer :: NumRep, fiddle with the definition of Num (and related things, not rehashing the problematic nature of Num ...) so that they apply at the new kind, and give all your numbers types like Quantity DOne Integer instead of Integer. The big advantage is that the type unification rules remain syntax-directed.

The second option seems justified for a green-field language design, even though it requires sweeping changes, because I can't think of a logical difference between a dimensionless 37 and a dimensionally naive 37 and because you can almost always erase the phantom type so there needn't be a performance problem. Question one: are there valid objections? Question two (bonus): literals that have the value 0 can be interpreted as polymorphic in their dimension, are there good objections for teaching the compiler about this rule? CSS is the only language I know of that does this, but it seems like a good idea.

When you start to track matrix sizes, you run into a similar problem where scalars and vectors start to look like degenerate matrices in the same way that dimensionally naive 37s are degenerate dimensioned 37s at dimension one. Adopting this convention recovers a single multiplication operator, saving you from scalar * scalar, scalar * vector, scalar * matrix, vector * matrix, matrix * matrix, and all the flipped versions. Scalar addition, inversion, and exponentiation maintain the same meanings if you look at them as degenerate matrix addition and exponentiation (at least for integer exponents?), and so do all the common trigonometric functions.

When you start to track matrix types for the non-uniformly dimensioned matrices I mentioned in the first paragraph, you end up realizing that matrix size checking falls out naturally from checking matrix dimensions (in the sense of physical dimensions) because you end up with an index type like MatrixShape :: Dim -> [Dim] -> [Dim] -> MatrixShape and your multiplication rule involves unifying the (normalized) "column dimensions" of the left operand with the (normalized) "row dimensions" of the right operand which happily takes care of the size checking.

This motivates the third question: what are the objections to treating all scalar numbers everywhere not only as degenerate dimensionless quantities, but as degenerate dimensionless matrices?

I have three objections so far:

• It means you probably can't use your Matrix type generator as a generic two-dimensional array type, ruling out things like Matrix String. You end up wanting to restrict the element type of the matrix to the kind of types-that-may-sensibly-carry-a-physical-dimension which may not overlap precisely with types-that-have-a-useful-Field-instance. (This may or may not be a bad thing, I'm not sure. Maybe the latter group of types could be plausibly interpreted as having a physical dimension?)
• Obviously you don't want to hit beginners with error messages that mention all the complicated phantom types just because they wrote "moose" + 3. (People have done a lot of interesting work on solving this problem, but it is still something to consider.)
• Does this go far enough? Or am I just unaware of the next-more-general concept of which matrices are a degenerate form? What justifies stopping here as opposed to not starting down this road in the first place?

TL;DR: Is 3 :: (Num a) => a really the most general type of 3?

Hi All,

I am pleased to announce the release of Pythonect 0.4.1, available from https://github.com/downloads/ikotler/pythonect/Pythonect-0.4.1.tar.gz

Release notes can be found at: https://github.com/ikotler/pythonect/wiki/What%27s-New-In-Pythonect-0.4.1

Many thanks to everyone who contributed bug reports, patches, and feedback that went into this release!

Hi all!

I built an interpreter for a language that is similar to lisp and scheme (https://github.com/bryanedds/aml/wiki). I am thinking about writing a .NET compiler for it, however I think I am missing some fundamental background knowledge. I think I can see how it might be smart to write an itermediate 'machine' that indirectly generates IL code rather than manually translating each special form to IL code directly. So instead of going from AST analysis straight to IL, I would go from interpreter to 'hand-wavy-virtual-machine' to IL. This stratification seems like a good idea, as it may ease optimization logic by reasoning about semantics at a lower level, but I don't know where to start.

Is there a typical stratification technique for building compilers for lambda calculus-based languages? It seems like it would look like an intepreter that passes symbolic primitive that are understood by a 'machine' that produces .NET code. Perhaps the SECD machine (http://en.wikipedia.org/wiki/SECD_machine) was something like this? I think Haskell's G-Machine might also be similar?

Am I off-base here?

PS - I'm still a language design newbie, so please keep any answers simple for me :)

I recently saw an inspiring presentation about how programming frameworks can help software developers, by providing more immediate feedback on the effect of changes to your code and better visualizations to understand what your code is doing. I found it thought-provoking, and I thought others here might, too.

Bret Victor, Inventing on Principle. CUSEC 2012.
http://vimeo.com/36579366

Enjoy!