Lambda the Ultimate

The idea of embedding a language with an ML-like type system in Lisp strikes me as very interesting. A small but significant amount of the code I write manipulates complex data structures, and in that code I think such a type system might be very helpful. I'd like to experiment with writing those parts with a static type system and embedding them in my regular dynamically-typed programs.

If the static typing fans are right that their way is better, it would also be a stepping stone towards that. Perhaps I could also put lazy evaluation and monads to good use, I don't know.

I hope Philip can be prevailed upon to post the code, or that some LtU reader has experience in this area to share. Like many Lispers, I don't really understand a language until I've seen it implemented in Lisp.

P.S., Philip Greenspun gets up a lot of peoples noses, but he is a very intelligent and accomplished guy. If you haven't already, you might like to look around his website. I found "The book behind the book behind the book.." particularly entertaining.

Compilers and complex syntax wasn't the right answer.

Simple syntax, and tools to help analyse, visualise, navigate and correct programmes is the right answer. It's just that we have put 30 or more years into the wrong answer and are all too red-faced to back out now.

http://www.simulys.com/guideto.htm

Type checking in Lisp

http://www.cs.indiana.edu/~chaynes/infer.html

I'm glad I posted it all the same: Qi is just the reference I was fishing for. Thanks Alex!

Same thing, but coming from the other end.

I have a personal preference for LISPs, but my experiences with OCAML persuaded me that working with a type inferred language is a very different experience for the developer than working with statically typed languages.

I draw the distinction, and I do respect the approach with ML, Haskell, etc. The biggest hurdle for me is that I am comfortable with dynamic languages and test-driven design. I am not sure how much more productive I would be with, say, Haskell.

At the same time the kind of programming I do most often requires writing extensions to Java and C# systems. A simple language like Jython or DotLisp supports exactly what I want. The "newer" functional languages don't seem to have as low a barrier to entry for this need, as far as I can tell.

Some day I expect these more sophisticated type systems to provide even more information and guidance than they do currently. I think it will take some order of magnitude leap in dynamic modeling functionality to get me to abandon something as simple as Smalltalk and SUnit.

G'Caml has nothing to do with dynamic typing.

Maybe I need to make an LtU FAQ for this sort of thing, though, frankly, I would never have expected someone to make this particular claim.

All the power of dynamic languages with an added check of "...and the objects/modules/... do in fact implement this interface".

It is about Interfaces, not Types as in the C#/Java sense.

It is about Interfaces, not Types as in the C#/Java sense.

The one fairly loose connection appears to be the use of runtime type information in the implementation. But I also thought the stated association with dynamic typing was misleading.

Maybe I need to make an LtU FAQ for this sort of thing, though, frankly, I would never have expected someone to make this particular claim.

G'Caml adds a dynamic type 'dyn', and a constructor/function to create them '$a -> dyn'. That is, dyn type carries both the value and its type. As far as I understand, this is the definition of dynamic typing. Do you disagree ?

You cannot pass these dynamic types as parameters to functions expecting specific static types. But you can create functions, that expect dynamic types as their parameters, creating the ability to make a dynamically typed sublanguage.

In the functions using the dynamic types as their proper static types, you have to first coerce them to their proper static types. This is done explicitly. If this is what concerns you, I would like to point out, that 'dynamically typed languages' such as Lisps, would do this very same thing, but implicitly.

Consider the complexity of parsing C++ for purposes of static analysis.

It is utterly devilish.

I would argue there is close relationship between the difficulty with which a program can make decisions on the correctness of a program and the difficulty with which a programmer can.

The whole trend to complex syntax arose from the history of how difficult it was to make decisions about the correctness of assembler programs.

So what viable alternatives have been demonstrated?

Joy.

Go to http://www.latrobe.edu.au/philosophy/phimvt/joy.html

In particular pay attention to Von Thun's papers on an Algebra for Joy and a Rewriting System for Joy.

Just as a tickler, here is his minimal joy in joy interpretor. Try write somthing like that in C++ and I'll see you a couple of thousand lines later...

joy0 == [ [ [ joy0 body joy0 ] [ [] ] [ pop pop pop ] [ cons pop cons ] [ opcase pop opcase ] [ body pop body ] [ i pop joy0 ] [ step pop [joy0] cons step ] [ [] cons i ] ] opcase i ] step

I agree that this is dynamic typing, but it is only one application of generic polymorphism and, I think, not a representative one. Indeed, you can do almost the same thing without genericity, as I once demonstrated here and here.

When embedding a dynamically typed language in a static host language, the difference between having genericity and not is that, with it, you can automatically embed all the user-defined datatypes of the host language, whereas without it you need to enumerate them manually. Most DT languages have a fixed set of built-in data types anyway, and to extend them you need to go outside the language.

Isn't that wrong for any dynamically checked language that supports OO?

note: I did notice the modifier, this is to check what I misunderstood

Implicit vs. explicit is the key difference.

I dunno. I guess it depends on what you mean by `OO' and `data type'.

Oh and, kudos for using the correct term `dynamically checked'. :) I should start doing this too.