Lambda the Ultimate

First off, I should qualify that I'm self-taught, and second that, budget permitting, LtU has been a major source of book purchases over the past few years(TaPL, CTM, EOPL,...). So, I've been working through these books in bit of a cyclical fashion(i.e. coming back to the parts I have no clue about and hoping they make sense this time...), and I avidly download and read papers that people link to from here(understanding them, of course, is entirely different matter).

Well, lately, I've developed a DSL for some of my work, and I think its all very innovative and unique, and I thought, "I should try and formalize the type system and semantics for this little language," and then I realized it: I have no clue.

I really just don't know what to do to formalize my language. Oh, I think I know the relevant concepts, I just don't know where to start.

Is there some book out there that would help with this(okay, I realize I may have already bought/read/skimmed said book, and densely missed the chapter, "How to Formalize Your DSL in 3 Easy Steps").

Forgive me if I just showed me ignorance or laziness, but this is what got me interested in programming language to start with(wanting to write down the formal semantics much the way I can write down the context free grammar), but this skill continue to elude me.

Perhaps my attempt to learn PLT by osmosis and waterfall method is not working out so great...

The indefatigable Bruce Eckel is learning all about Java generics so he can write about them in a way that explains things to mere mortals. It is clear to me that the Average Joes who have been using Java are going to have their minds blown by such things, and I wonder if Java has taken a large step along the pirate ship plank off to C++-like complexity and confoundedness? Along this vein of thought, advanced functional languages don't get much use in industry and I think people attribute it party to their tougher learning curve.

So my question is, at what point have you made a language that regular folks simply won't be willing to learn? And the challenge is, how can languages be designed to give advanced benefits yet hide the complexities? Why can't machines better hide issues like co vs. contra variant type usage (or whatever)?

The main Haskell and ML compilers integrate many extensions to Hindley-Milner, but many other extensions are left out: intersection types, basic (DML or ATS) dependant types, constraint-handling systems like HM(X), generic types, subtyping … Some of these are new, but some of them are older than other extensions that are getting integrated into mainstream compilers. What happens to these ideas after their toy compilers leave town?

Also, why do the main compiler projects not integrate work done in each other &mdash Why doesn't SML have type classes? Why doesn't GHC have polymorphic variants?

My guess for the first question is that the work necessary to code a new type inferencer is less than what it takes to integrate a new type inferencer into a pre-existing compiler. Pushed by grant or graduation deadlines, the simpler work is done. In the meantime, people like Simon Peyton-Jones beg for GHC hackers.

As for the second question, I suspect there's a little bit of NIH syndrome acting together with grant pressure &mdash row types in HM is already done in O'Caml, why would ICFP publish a paper about doing the same thing in Haskell?

Of course, perhaps the most valuable extensions are being integrated, or perhaps these things are a matter of chance, as interests and Ph.D. students come and go.

I was hoping to get some advice about a dilemma I'm in. I'll be entering a Ph.D. program next fall (hopefully), and I'm already having trouble finding summer internships because few companies want to take on interns that 1. are just starting their research careers and 2. won't be available for full-time work for many years. Have any of you been in a similar situation or have any thoughts about it?

Hi there,

Sorry to pester y'all, but I was hoping I might get some citation-type help. I realized for my little pet language that I'm working on that need to do some homework on conjunction types, but I can't find any publicly-available articles on the topic. Does anyone know off of the top of their heads any friendly introductions to these types that doesn't require IEEE or ACM membership to read?

Thanks in advance,

JimDesu

I've been reading a lot about various new languages like Ruby, Haskell, Python, etc. But none of them seem suitable for programming say, an Operating System, or performing really low level work on an embedded device. First, these languages (understandably) sacrifice efficiency for ease of use (but I don't think these are always mutually exclusive). Second, a lot of times these languages simply don't provide any mechanism for getting at the hardware.

Has there been any research into new languages that would be as suitable for an OS as C?

I am pondering over some non-serious application of Curry-Howard isomorphism (CHI). Let's take any typical text in a natural language. What is its contents? Propositions or proofs? My judgement is that (almost?) exclusively propositions. Applying CHI, we can see that humans write mostly types. Already sounds strange.

Now, instead of a static text, let's analyze an interaction in a natural language (e.g., a conversation over a phone). People are still exchanging propositions, i.e., types. From this point I am trying to get back to computer science. Why isn't it so common that programs exchange types over the wire? Or rather, why cant we naturally see any programmatic interaction as an exchange of (exclusively) types? I suspect we can argue that transmitted values are just witnesses of the corresponding types, but still it is not natural, or at least traditional way to look at the issue. Why? Or did I make some mistake during my analysis of natural language part of the problem?

I know that "programmatic interaction" can be seen as a proof-reduction, but I am currently wearing more message-oriented hat.

I just had an interesting phone conversation with a friend of mine concerning the building of robost software (architectures, applications) and how the process could relate to language design.

We started listing a checklist of criteria (whether required or merely wanted) and we came up with a few items. We had a simple criteria of program correctness, program maintainence (comprehension), and modularity.

For program comprehension/correctness:
Strong typing
Purely functional
Strict evaluation
Design by Contract came up as a possibility
Verbose error messages

For modularity:
Objects were a thought, but it was felt the same architectures could be achieved with types, functions, and modules

These were just a few of the things that we thought could help in building large scale applications and frameworks, but both my friend and I lack the desired amount of experience to develop a stricter and more verbose criteria.

I was wondering what everyone's elses opionion would be concerning this topic.

If you had to build a large software architecture/application what kind of 'features' would you look for in a language?

Best regards,

MJ Stahl

It's been a long while since I've looked at Logo. Somehow I ended up here. Logo is often considered only a toy language. But, while it doesn't have the expressiveness of it's closest cousins Scheme and Lisp, simplicity has it's place.

In primary/secondary education, Squeak Smalltalk seems to be taking away the Logo mindshare (at least it seems this way). Is this true?

Are there any network transparent languages apart from Mozart(Oz) and Google's Sawzall(to some extent).I have tried searching on this subject, but nothing significant turned up.I have not even found any references to such languages in any of the programming language (text) books.

I would be glad if anyone can answer the following questions:
- Are they different from languages which support distributed programming?
- Why are they not popular, i feel that such a language has very interesting and practical applications.( like run-time load balancing of applications etc..)
- Are there any theoritical/practical reasons why they will not be useful, even if one exists?

Any other pointers will also be helpful.