Lambda the Ultimate

G'Caml, which extends O'Caml with overloading, has been around since O'Caml 2.0something. It is now updated with its own source code (no more patching!) and some new features (generic primitives?) that I don't understand.

I think I remember seeing Simon Peyton-Jones predict somewhere that ML would grow type classes. Will G'Caml metastasize?

I didn't see anyone post them yet, so here are the slides from Tim Sweeney's POPL talk entitled "The Next Mainstream Programming Languages: A Game Developer's Perspective". I know Tim and I aren't the only game developers who follow LtU, and I figure even non-game developers might find them quite interesting!

http://www.cs.princeton.edu/~dpw/popl/06/Tim-POPL.ppt

What is a monad, why should I use it, and when is it appropriate?

Can anyone answer this in a post without showing code? And if possible, relate it to OO concepts like classes and delegates.

If you read between the lines (even if you don't) in Don Syme's blog post (near the end) he talks about DLinq and the use of quotation, abstract syntax and stuff like that.

In the C# 3.0 spec the Expression trees (26.8) are slipped in right at the end with the promise of another specification to describe them.

While studying OO at university, it was drilled into me that I should "package data with the methods that operate on that data".

In recent years I have come to wonder why so much emphasis is placed on this concept.

For example, most 3D Vector classes I have encountered look something like:

class 3DVector
{
private float X;
private float Y;
private float Z;

public 3DVector Normalize();
public 3DVector Add (3DVector other);
public float Dot (3DVector other);
... etc
}

This appears well organised.. Various methods that act on a 3D vector nicely packaged up together. I'm guessing most OO programmers would generally approach class design in this way.

But at the same time, its very hard for multiple vendors to add their own functionality to the class, they are forced to collaborate and merge their methods into the "current version".

In this instance, would it not be more sensible to have something like:

class 3DVector // Agreed, Never going to change
{
public float X;
public float Y;
public float Z;
}

---- Vendor (1)

3DVector Vendor1_3DVector_Normalize (3DVector v)
3DVector Vendor1_3DVector_Add (3DVector a, 3DVector b)
float Vendor1_3DVector_Dot (3DVector a, 3DVector b)

---- Vendor (2)

3DVector Vendor2_3DVector_Cross (3DVector a, 3DVector b)
float Vendor2_3DVector_Length (3DVector v)
3DVector Vendor2_3DVector_Dot (3DVector a, 3DVector b)

Then as a vendor, you are able to release new functions as and when you please.

As an application developer, you are free to pick and choose those functions that fit your requirements, or add your own.

The vendors would have to collaborate on the initial "Data Format" of a class, but once settled, an eco-system of functions would build up that operate on it.

I realise this is a simplistic example, and can see it would be hard to extend the idea to more complex objects with state. But I was curious whether there are any real-world OO systems that leverage this sort of thing, and how far they take it?

My Google Alert on Haskell tortured me with weeks of unrelated news about folks called Haskell, sports results from a college of the same name and local incidents from a town of the same name. Finally today I got a on-topic hit. Allow me to share it with you, it is here.

PS Is this is the proper way to submit some interesting link?

U is a small (< 1000 words) computational model:

http://urbit.sf.net/u.txt

U is different because it:

• has no user-defined functions or lambda
• has a built-in hyper-Turing operator
• expects an unreliable packet network

I have to apologize for posting this weird beast with no real context. I'm working on higher layers that should make its purpose clearer, but they are not done, and we all hate hand-waving. Still, the U spec is self-contained, and it should be precise and readable. If anyone can look at it and maybe even find some gotchas, I'd be super grateful.

I'm especially curious about the follow operator. Are there any logical flaws in its definition, or ways it could be improved, generalized or tightened?

Also, if anyone knows of any other UDP-level functional languages, or anything else U reminds them of, I would of course be happy to hear it.


Thanks,
Curtis
(curtis dot yarvin, at gmail)

So... how big can dynamically-typed systems get? Do static type systems really matter? I'd love to know the answer to this.

We have some big systems at Amazon, and most of them seem to use strong static typing; at least the ones I know about do. Is that a requirement, or could we just as well have done them in Perl, Ruby, Lisp, Smalltalk?

Read more about it here.

In a series of papers, Jean Goubault-Larrecq has established a relationship between modal logic systems and type systems for metaexpressions, i.e. (quasi-)quoted expressions. I will use a pseudo Lisp syntax and furthermore I will write quote for both quote and quasiquote. In such systems, if (has-type (quote x) (quote A)), then (has-type (quote (quote x)) (quote ([] A))), where [] is a modal operator. One can read "([] A)" as "a representation of an A". The unquote is the corresponding destructor.

It appears to me that modal operators are merely syntactic abbreviations for predicates on propositions, i.e., ([] A) is merely an abbreviation for (P (quote A)) where P is some corresponding predicate on propositions. For example, the modal operator in provability logics can be identified with the |- provability predicate: to express that A is provable one can write either (|- (quote A)), or ([] A). A proposition thus has type (quote (|- (quote bool))).

(By the way, if we treat predicates/sets as characteristic functions, then modal operators are really evaluators, and |- with two relands is an evaluator with an environment. A partially applied type-assignment relation (has-type (quote x)) then corresponds to a modal operator [(quote x)] that has a term as a parameter.)

The proof rules rules for minimal logic in their most basic form (with a single proposition instead of a context) look like the following:

(has-type (quote make-x) (quote (|- (quote P)))) 
(has-type (quote make-y) (quote (|- (quote Q))))
; ... other assumptions

(has-type (quote i→)
          (quote (∀ a (|- (quote bool))
                   (∀ b (|- (quote bool))
                     (→ (→ (|- a) (|- b))
                        (|- (quote (→ (unquote a) (unquote b)))))))))
(has-type (quote e→)
          (quote (∀ a (|- (quote bool))
                   (∀ b (|- (quote bool))
                     (→ (|- (quote (→ (unquote a) (unquote b))))
                        (→ (|- a) (|- b)))))))

Now it becomes clear that proof rules are the types of the constructors of the proofs (terms) in a language. For example, (e→ (quote (→ A B)) (quote A) (quote f) (quote x)) denotes (quote (f x)) The first two arguments are there because e→ is polymorphic, but they can be left implicit.

The written representation of an abstraction term is now problematic because the abstraction term contructor i→ takes a function of type (quote (→ (|- (quote A)) (|- (quote B)))) as argument, not a (sub)term. To write down a abstraction term we would have to write the written representation of a function. This implies it is impossible to write down abstraction terms.

We can resort to a trick to be able to write some abstraction terms indirectly. Here the substitution function comes to the rescue. Most generally, subst takes five arguments: (subst (quote A) (quote B) (quote x) (quote M) (quote N)). The two types (quote A) and (quote B) are given because subst is polymorphic and it must be specified what is the type of (quote x) on the one hand and (quote N) and (quote M) on the other hand. I will sometimes leave them implicit as in other situations.

Partially applying subst to four arguments, the resulting term has the required type (quote (→ (|- a) (|- b))). Thus the term (i→ (quote A) (quote B) (subst (quote A) (quote B) (quote x) (quote M))) is correctly typed and is a abstraction term that does what you expect.

This explains the strange shape of λ terms: a λ term is actually a macro (i.e. syntactic abbreviation) for a term that cannot be written, somewhat as follows (the output type b is inferred):

(defmacro λ (x a m))
  (i→ (subst a b x m)))

Note the absense of quotes in the body. Alternatively, we can add a new `λ reduction' rule (the output type b is inferred):

(∀ ... (→λ (quote (λ (unquote x) (unquote a) (unquote m)))
                  (i→ (subst a b x m))))

This explains the shape of the beta reduction rule:

(∀ ... (→β (e→ (quote (λ (unquote a) (unquote x) (unquote m))) n)
               (subst a b x m n)))

This is because this rule is merely a special case of a more general rule for beta reduction:

(∀ ... (→β (e→ (i→ f) n) (f n)))

or, even more generally,

(∀ ... (→β (e→ (i→ f)) f))

or even something like:

(∀ ... (→β (° e→ i→) id))

By the way, the type assignment rules then become:

(has-type (quote t-make-x) (quote (has-type make-x (quote P))))
(has-type (quote t-make-y) (quote (has-type make-y (quote Q))))
; ... other variable declarations
(has-type (quote ti→)
          (quote (∀ ...
                   (→ (→ (has-type x a) (has-type (f x) b))
                      (has-type (i→ f) (quote (→ (unquote a) (unquote b))))))))
(has-type (quote te→)
          (quote (∀ ...
                   (→ (has-type f (quote (→ (unquote a) (unquote b))))
                      (→ (has-type x a) (has-type (e→ f x) b))))))

Does anyone know which OO languages support a-posteriori subtyping? In other words the creation of new subtype relationships between classes without modifying existing classes. Thanks a lot!