When programming, I often find myself striving for minimalism. Trying to make the program as succinct as possible, sweating over details like how to arrange the sections in a file, or the number of files to create.
But minimalism in programming may cause programs to appear cramped, may persuade you to choose forms of expression that are unneededly terse, and may also lead to programs that are hard to refactor or extend.
Point is, when you start programming, you don't know how big the program's gonna be, so starting with minimalism may be a bad choice. When looking at the sources of some huge programs, I found that some of them have found very relaxed ways to deal with their sprawling size. Gnus for example comprises dozens of large source files, containing hundreds or thousands of operational definitions, and yet remains very readable.
I don't want to get into the details of architecting large programs - I'd rather like to focus on a way to write programs, from the start, so that the source then has a "density" that's adequate to its size. Gnus for example is meandering, and that's perfectly adequate - Gnus being a mail reader for the most customizable OS in existence. That's a job that's never done, so the source should reflect that - you can't write a cute blog post about a program like Gnus, there's no single overarching, minimalist design principle.
Maybe, as Perlis said, every program needs to be written at least twice. After the first run, we know the approximate size of the program, and can then find a code density/terseness that's adequate to that size.
I find minimalism in source code is often limiting. In my next program, I'll write it from the start as if it were really huge.
Manuel Simoni's blog about programming (languages).
Monday, September 27, 2010
Linus on transactional memory
I want transactional memory like the next guy, but comments like this one by Linus indicate that we still have a long way to go:
So that's what it boils down to: transactions are "free" and a wonderful way to elide those horrible expensive locks.
But only if you never make a mistake.
They are expensive as hell even for very low rates of transaction failures. And you really cannot know statically (even if you don't end up reaching some transaction limit, you may easily end up just having heavy contention on the data structures in question).
So I claim that anybody who does transactional memory without having a very good dynamic fallback is basically totally incompetent. And so far I haven't seen anything that convinces me that competence even exists in this area.
Monday, September 20, 2010
The ghosts of blog posts past
Ah, blogging. On the one hand there's value to reading someone's opinion unfiltered and raw. On the other hand it creates a lot of friction, and pisses people off.
This is a blog. It is a special medium. I'm not writing articles, which I expect to stand the test of time. I don't let my friends preview the posts I write, and point out their problems. Because I think there's a difference between writing articles (as, say, Paul Graham does) and blogging. And both have merits. This is a blog.
It presents my opinions and mood at a specific point in time. If you don't like it, argue with me, but don't take it too seriously. Take my posts like snarky or humorous remarks over a beer. That's how I write them. Because that's what I think is one of the things blogs are good for, and that's how I'm running this particular blog.
-- Manuel
This is a blog. It is a special medium. I'm not writing articles, which I expect to stand the test of time. I don't let my friends preview the posts I write, and point out their problems. Because I think there's a difference between writing articles (as, say, Paul Graham does) and blogging. And both have merits. This is a blog.
It presents my opinions and mood at a specific point in time. If you don't like it, argue with me, but don't take it too seriously. Take my posts like snarky or humorous remarks over a beer. That's how I write them. Because that's what I think is one of the things blogs are good for, and that's how I'm running this particular blog.
-- Manuel
Monday, September 13, 2010
The far side of the lambda cube
Of course, once you investigate higher-order types, you begin to think about unifying the type and term levels.
Reading a bit about this I found some interesting links:
Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and Dynamic. A recent paper I found via Ahmed, Findler, Siek, and Wadler's new Blame for All. I find the use of a counter-example database in a compiler a bit frightening, though.
Henk: A Typed Intermediate Language, from 1997, by SPJ and Erik Meijer:
And, Your lambda-cube is puny.
Reading a bit about this I found some interesting links:
Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and Dynamic. A recent paper I found via Ahmed, Findler, Siek, and Wadler's new Blame for All. I find the use of a counter-example database in a compiler a bit frightening, though.
Henk: A Typed Intermediate Language, from 1997, by SPJ and Erik Meijer:
There is growing interest in the use of richly-typed intermediate languages in sophisticated compilers for higher-order, typed source languages. These intermediate languages are typically stratified, involving terms, types, and kinds. As the sophistication of the type system increases, these three levels begin to look more and more similar, so an attractive approach is to use a single syntax, and a single data type in the compiler, to represent all three.Languages of the Future, by Tim Sheard on Omega, on which I'll post something soon.
The theory of so-called pure type systems makes precisely such an identification. This paper describes Henk, a new typed intermediate language based closely on a particular pure type system, the lambda cube. On the way we give a tutorial introduction to the lambda cube.
And, Your lambda-cube is puny.
A moment of respectful silence, please.
Sunday, September 12, 2010
Higher kinds are sexier
In the process of formalizing generics for my Lisp, I'm also studying FGJω again, the extension of Featherweight Generic Java with higher kinds. Instead of just parameterizing types with first-order types, such as T, you can parameterize types with type-level "functions", such as F<T>. One example of such a function is the type List<T> - you give it a T, and it "returns" the concrete type of lists containing that type.
And it turns out, the theory behind that looks simpler, and thus sexier:
It's kinda embarrassing to post this stuff here, since I'm so bad at type theory, but I think I can make it work. One insight giving me this faith is that none of this stuff survives till runtime: at runtime, only concrete instantiations, such as List <String> remain. Or so I hope.
And it turns out, the theory behind that looks simpler, and thus sexier:
(types) T ::= (K K*)I like the definition of types: a type's the application of a constructor to zero or more other constructors. Constructors may be variables (X), classes (C), or functions taking zero or more parameters and returning a type. (So you basically have a lambda calculus at the type-level.) A type parameter is a variable constructor with zero or more parameters, optionally bounded to a class type with zero or more type arguments. Class definitions are parameterized over zero or more type parameters, and extend zero or more existing classes. (I'm taking some liberties with adding multiple inheritance, hoping it doesn't mess up the theory. :P) Method definitions are, as usual, parameterized on the type- and term-level and have a result type.
(type constructors) K ::= X | C | (P* => T)
(type param defs) P ::= (X P*) | (<: (X P*) (C K*))
(class defs) D ::= DEFCLASS (C P*) ((C K*)*)
(method defs) M ::= DEFMETHOD (m P*) ((param T)* -> T)
It's kinda embarrassing to post this stuff here, since I'm so bad at type theory, but I think I can make it work. One insight giving me this faith is that none of this stuff survives till runtime: at runtime, only concrete instantiations, such as List
Friday, September 10, 2010
Formalizing generics
In the previous post, Minimal generics for an untyped language, I've discussed some basic requirements for the implementation of parametric polymorphism in the Lisp I'm working on.
I've now made some progress in formalizing this, based on Featherweight Generic Java. Here's a basic overview of the type system in the FGJ style:
Type parameters in a class definition or method definition (X) are scoped over the entire definition, including the bounds (in the style of F-bounded polymorphism).
All of this is pretty much equivalent to FGJ. The only difference is that classes do not contain methods.
[Updates: I've added type parameterization to method definitions. Added Top. Added some parentheses to make the syntax unambiguous.]
I've now made some progress in formalizing this, based on Featherweight Generic Java. Here's a basic overview of the type system in the FGJ style:
(types) T ::= C | X | TopTypes are either class types (C), type parameters (X), or Top. Class types have a name (klass) and zero or more types as parameters. A class definition introduces a named class, parameterized over zero or more type parameters that have class types as bounds, zero or more superclass types, and zero or more named and typed slots. A method definition introduces a named method, parameterized over zero or more type parameters that have class types as bounds, with zero or more named and typed parameters and a result type.
(classes) C ::= (klass T*)
(class defs) D ::= DEFCLASS (klass (<: X C)*) (C*) ((slot T)*)
(method defs) M ::= DEFMETHOD (method (<: X C)*) ((param T)* -> T)
Type parameters in a class definition or method definition (X) are scoped over the entire definition, including the bounds (in the style of F-bounded polymorphism).
All of this is pretty much equivalent to FGJ. The only difference is that classes do not contain methods.
[Updates: I've added type parameterization to method definitions. Added Top. Added some parentheses to make the syntax unambiguous.]
Wednesday, September 8, 2010
Minimal generics for an untyped language
So, I'm developing a Lisp, which means I have to support untyped, dynamically type-checked code in any case. But I still like typeful programming.
Generics, or parametric polymorphism, are jolly useful, even on a totally limited scale: all I want from the first round of this endeavor is to support something like the following:
(defclass (list T))
(defmethod add ((list (list T)) (element T))
...)
Here, I define the class (list T) - a list parameterized over the type of its elements, T. That's the same as Java's List<T>. The method ADD takes such a list and an element, and adds it to the list.
To create an instance of a parameterized class, you have to pass a concrete type argument to use for the element type, as in:
(defvar *my-list* (make (list string)))
This creates a list that accepts strings (and instances of subclasses of string) as elements.
The instance has to remember that it's a list of strings for type safety. When ADD is called on a list, the runtime needs to check that the element type matches:
(add *my-list* "foo") ;; OK
(add *my-list* 12) ;; runtime error
One more thing I'd also like is the following;
(defclass (foo (<: X bar)))
That's a class foo that has one parameter, that must be a subtype of bar, analogous to Java's Foo<X extends Bar>. Being able to give such a bound to a type parameter seems quite essential.
Furthermore, it has to be possible to pass on type parameters to superclasses, as in:
(defclass (super-1 T))
(defclass (super-2 T))
(defclass (klass X Y) ((super-1 X) (super-2 Y)))
(klass X Y) is parameterized over two types, X and Y, and passes them on to its two superclasses, each of which is parameterized over one type.
Of course, it also has to be possible to remove parameterization, as in:
(defclass string-list ((list string)))
This defines an unparameterized class string-list, which is a subclass of (list string).
Another requirement is that it has to be possible to create instances of type arguments, as in:
(defclass (klass T))
(defmethod make-a-new-t ((k (klass T)))
(make T))
That's just cute, and may have some applications to dependency injection.
I'd also like to be able to write polymorphic functions:
(defun identity ((a T) -> T) a)
The arrow indicates the result type of the function. In this case it takes an instance of any type and returns it.
It should also be possible to give slots (member variables) of classes the types of type parameters:
(defclass (klass X Y) ()
((slot-1 X)
(slot-2 Y)))
This defines a class with two type parameters X and Y, (no superclasses,) and two slots slot-1 and slot-2 with the types X and Y, respectively.
These are the basic requirements. Now I need a plan! ;)
Generics, or parametric polymorphism, are jolly useful, even on a totally limited scale: all I want from the first round of this endeavor is to support something like the following:
(defclass (list T))
(defmethod add ((list (list T)) (element T))
...)
Here, I define the class (list T) - a list parameterized over the type of its elements, T. That's the same as Java's List<T>. The method ADD takes such a list and an element, and adds it to the list.
To create an instance of a parameterized class, you have to pass a concrete type argument to use for the element type, as in:
(defvar *my-list* (make (list string)))
This creates a list that accepts strings (and instances of subclasses of string) as elements.
The instance has to remember that it's a list of strings for type safety. When ADD is called on a list, the runtime needs to check that the element type matches:
(add *my-list* "foo") ;; OK
(add *my-list* 12) ;; runtime error
One more thing I'd also like is the following;
(defclass (foo (<: X bar)))
That's a class foo that has one parameter, that must be a subtype of bar, analogous to Java's Foo<X extends Bar>. Being able to give such a bound to a type parameter seems quite essential.
Furthermore, it has to be possible to pass on type parameters to superclasses, as in:
(defclass (super-1 T))
(defclass (super-2 T))
(defclass (klass X Y) ((super-1 X) (super-2 Y)))
(klass X Y) is parameterized over two types, X and Y, and passes them on to its two superclasses, each of which is parameterized over one type.
Of course, it also has to be possible to remove parameterization, as in:
(defclass string-list ((list string)))
This defines an unparameterized class string-list, which is a subclass of (list string).
Another requirement is that it has to be possible to create instances of type arguments, as in:
(defclass (klass T))
(defmethod make-a-new-t ((k (klass T)))
(make T))
That's just cute, and may have some applications to dependency injection.
I'd also like to be able to write polymorphic functions:
(defun identity ((a T) -> T) a)
The arrow indicates the result type of the function. In this case it takes an instance of any type and returns it.
It should also be possible to give slots (member variables) of classes the types of type parameters:
(defclass (klass X Y) ()
((slot-1 X)
(slot-2 Y)))
This defines a class with two type parameters X and Y, (no superclasses,) and two slots slot-1 and slot-2 with the types X and Y, respectively.
These are the basic requirements. Now I need a plan! ;)
Tuesday, September 7, 2010
Fast dynamic casting
Fast dynamic casting, a cute paper by Michael Gibbs and Bjarne Stroustrup:
Relatedly, I've also been thinking about using perfect hashing to implement multiple dispatch. It should work just fine, and actually reduce the number of type tests, compared to single dispatch. Unforch, I'm still in the make-it-work phase, which is followed by the make-it-correct phase. Only then does the glorious make-it-fast phase start.
We have demonstrated that it is possible for a linker to generate integer type IDs for classes such that it may be verified by a simple integer modulo computation that one class derives from another in an object-oriented language. When combined with a suitable way of adjusting offsets, this method provides for a fast, constant-time dynamic casting algorithm. A 64-bit type ID is capable of representing quite large class hierarchies containing thousands of classes and at least nine levels deep.I knew that prime numbers could be used for this somehow, but these guys have already worked it out.
Relatedly, I've also been thinking about using perfect hashing to implement multiple dispatch. It should work just fine, and actually reduce the number of type tests, compared to single dispatch. Unforch, I'm still in the make-it-work phase, which is followed by the make-it-correct phase. Only then does the glorious make-it-fast phase start.
Monday, September 6, 2010
Programmer feel-good quote
From a bit to a few hundred megabytes, from a microsecond to a half an hour of computing confronts us with completely baffling ratio of 109! The programmer is in the unique position that his is the only discipline and profession in which such a gigantic ratio, which totally baffles our imagination, has to be bridged by a single technology. He has to be able to think in terms of conceptual hierarchies that are much deeper than a single mind ever needed to face before. — E.W. Dijkstra
Sunday, September 5, 2010
Saturday, September 4, 2010
The many forms of polymorphism
It's important to realize that different kinds of polymorphism in type systems can be quite orthogonal.
Here are some forms of polymorphism, from Types and Polymorphism in Persistent Programming Systems by R.C.H. Connor:
Here are some forms of polymorphism, from Types and Polymorphism in Persistent Programming Systems by R.C.H. Connor:
ad hoc: An operation is defined over a number of different types, and its semantics may depend upon the type of its operands. An example is the operator "+", which may be defined over integers and reals, and has a different interpretation for each type.He further writes:
parametric: Instances of the same type within a type description may be abstracted over by an implicit or explicit type parameter. An example is an identity function, where although the parameter and result may be of any type, they are statically known to be the same type.
inclusion: The type of a value may be partially abstracted over, so that unnecessary type information need not be stated. An example is a function which is defined over any record value which has an age field of type integer.
All of these language concepts have evolved independently from each other. Languages such as early assemblers contained no polymorphism whatsoever. Ad hoc polymorphism was the first to appear, in languages such as Fortran, which defined overloaded operators, such as "+", along with the ability to coerce values from integer to real according to the use of such operators. Parametric polymorphism appeared in ML, and inclusion polymorphism in Simula. Existentially quantified types as described by Mitchell and Plotkin is a model of abstract data types which introduces abstraction over a type description, and such types are included in the definition of parametric polymorphism given above.
The motivation for all of these diverse language models is the same: the need to abstract over type. As type systems include more static constraints, then flexibility is lost as well as safety gained. Some of this flexibility, however, may be regained without the loss of safety by the introduction of type abstraction. Polymorphism is viewed here not as some theoretical attribute of type systems but as a solution to a class of practical problems which require type abstraction.
Friday, September 3, 2010
From Choosing VMs to Feng Shui for HCI
There's a nice discussion going on in the LtU thread Choosing a VM for a concurrent language. Some quotes, out of context:
Sean McDirmid:
Sean McDirmid:
I'm sick and tired of PL papers that present a novel language idea and then justify it with...a formal model...huh? This is a logical fallacy of the shaggy dog variety.David Barbour:
developing a new language is also nigh completely pointless unless there is something useful and interesting you can say about it. ...Matt Hellige:
Usage doesn't justify a design. Valid technical design seems to be a relatively minor factor in market success. ...
most attempts to achieve 'ease-of-use' and 'ergonomics' involve guidance by reasoned principles... a sort of Feng Shui for HCI (which holistically includes PL).
Programming languages are tools that require significant investment of time to learn to use well. To a large degree, their value is measured in terms of how valuable they are to the people who know them best.