Lambda the Ultimate

I am trying to build a simple DSL in scheme. I would like this DSL to use type inference to constrain s-expressions to only those that are provably type correct. My type scheme is fairly simple. I would like to have the following basic polymorphic types (at least for starters. This will likely expand later):

datum
  number
    real
      int
  char
  bool

In addition, I would like to support functions (all curried to a single param), lists and intersections of types, so that types like (-> int char) and (intersection (list-of int) char) can be supported. Strings will be lists of char for my DSL.

I know the way to do this is to use a type unification algorithm. Unfortunately, all the docs I can find on this subject seem to be very much research oriented and way over my head since I do not grasp the basic concepts here. I am wondering if anyone has some pointers to some good type inference tutorial level stuff that I might be able to get a good grasp of the basic principles and algorithm from.

Hi,

I just spent the last semester learning about category theory and concurrency , and I'm still confused by the whole thing.

But I put together my notes in an effort to practice my writing and straighten out some of my thinking, so I figured I'd post them here to see if they'd interest anyone.
There are definitely a lot of 'not-quite-right' details inside.

Brief Announcement: Secondlife(.com) now has an LTU-equivalent discussion group "Lambda The Ultimate"
Enrollment is free and open to all.

Dear LtU,

My google search didn't answer my doubts so I am posting here my question.

When we see a program, especially in imperative languages, we are often very fast in determining his computational complexity. Other times the same job is very hard.
My question is about the logic process that we follow in determining the computational complexity of a program/function.
(Of course i mean the complexity of the worst case only).
I am searching for somewhat very similar to the Hoare Logic.
A sort of formal logical system for derive judgments like P \in O(n^2) ... where n is the length of the Input.

This system should make clear the informal steps we use every days in determining the complexity of a function (especially in imp. languages).

I don't know if Hoare Logic can be directly used to this purposed. Maybe it's possible and we don't need a different formal system.

Thanks for any help.

Matteo

Happy New Year!

I just found that I am again reinventing a wheel, this time it is delay construct featured in ECLiPSe.
Quick searching revealed that similar constructs are available in various PLs (freeze in Prolog-II, when in NU-Prolog, block in SICStus, bind hook(?) in ESP, committed choice/guards in other PLs).

Is there a survey of these mechanizms out there, or the only way to learn the differences between them is to read the manuals of all these PLs?

Any help is appreciated.

How much implicit parallelism is there in functional programs?

One answer is "lots (I'd imagine)." Functional languages (and especially non-strict functional languages) can place relatively few constraints on a program's order of evaluation, often allowing multiple evaluations to proceed in parallel--at least in principle. The resulting "implicit" parallelism may be easy and useful to locate and exploit.

Another answer is "not so much (in actual experience)." When you take an existing, non-trivial functional program and try to find practical ways to speed it up by judicious placement of `par` (or by strategies or whatever), a surprisingly large effort can produce a surprisingly small improvement. So maybe that implicit parallelism just isn't there.

Another is "well, maybe it's there but it's just hard to find." If people can't find much implicit parallelism in real software, maybe it's the fault of the people. Maybe `par` and strategies and such are just too hard for people to use. Maybe some automatic parallelization mechanisms, yet to be invented, could do much better. Or something.

One interesting new answer is "I don't know. Let's measure it." I've just written a short paper on measuring the implicit parallelism in real Haskell programs, such as the NHC98 compiler. These measurements are in the context of a limit study, so they let us say that there is _no more_ than some certain amount of implicit parallelism present; exploiting even that much might of course be impractical.

The paper is at http://www.detreville.org/papers/Limits.pdf. I'd appreciate comments, of course.

Cheers,
John

Here is a paper explaining the addition of lambdas to Forth.

In the non-academic space, my language Enchilada has postfix lambdas via the eager macro operator.

Interestingly, Enchilada can avoid the name capturing problems that plague Lisp macros (although some Lisp hackers love name capturing). Moreover, the detection of name capturing is done very efficiently in Enchilada.

Enchilada macros bind with numbers and lists but not with other macros or operators. But because Enchilada lists hold expressions, macros can be indirectly bound to other macros.

Here is a simple (postfix) Enchilada macro:

5 3 {a b=b a - +}
5 {a=3 a - +}
3 5 - +
3 _5 +
_2

macro variables have lexical scope:

1 2 3 {a={b={c=a b c}}}
1 2 {b={c=3 b c}}
1 {c=3 2 c}
3 2 1

macros can be reduced eagerly:

[1] [2] [3] {a b c==[a] b [c] + +}
[1] [2] [3] {a b c==[a] b [c] + +}
[1] [2] {a b==[a] b [[3]] + +}
[1] {a==[a;2;[3]]}
[[1];2;[3]]

and name clashes are avoided by automatic alpha-conversion:

1 2 {a==[a] {a b=a b}}
1 2 {a=={aa=aa [a]}}
1 {aa=aa [2]}
1 [2]

passing and lifting(^) a macro into another macro:

1 2 [{a b==b a}] {d e f==[d] [e] f ^}
1 2 [{a b==b a}] {d e f==[d] [e] f ^}
1 2 {d e==[e] [d]}
1 {d==[2] [d]}
[2] [1]

Enchilada started as a language similar in design to the Joy language. But I think with macros on board it boosts the expressive power of Lisp.

Are there any current metrics available for programmatic complexity? For example, there are computational complexity classes for different types of programs, and big-Oh notation for runtime complexity of different algorithms, but is there a measure of how hard it is to actually program a given task in a given system?

For example, let's say the task is converting a list of numbers representing miles into kilometers. In C++, the code would be something like

float *miles_to_kilometers(float[] mile_list, int length) {
  float *kilo_list = new float[length];
  for(int i = 0; i < length; i++) {
    kilo_list[i] = mile_list[i] * 1.61;
  }
  return kilo_list;

In Perl, it would be something like:

sub miles_to_kilometers {
  my @result = map { $_ * 1.61 } @{$_[0]};
  return \@result;
}

My intuition would be that the Perl version would have a lower programmatic complexity because the loop is built-in rather than explicitly coded. Is there a metric available that evaluates such propositions?

In the posting, Quotation and evaluation -- or, how pure is the pure lambda calculus? (http://lambda-the-ultimate.org/node/1930), i mentioned that i saw quotation as a means of structuring name-free accounts of computations that provided a way of preserving the base term structure. i see preserving term structure as a very important property. In my experience an algebraic means of expressing computation comes to the fore because there is something in the syntax that aligns well with the semantics it expresses. Users, programmers, designers, analysts can think through the syntax to the semantics. So, preserving whatever it is that the syntax got right is part and parcel of preserving the arc of development of the notion of computation. Further, to my way of thinking each notion of computation is not just situated in a larger space of notions of computation but its form predicts, to a large degree, how the notion of computation will evolve, and therefore how our understanding of computation as captured in said notion evolves. The π-calculus captures computation as process. Petri-nets capture computation as token flow. And, the λ-calculus captures computation as (a kind of) function.

To illustrate how preserving term structure sets up an arc of the development of our ideas about computation i want to reveal some structure that was already implicit in the lambda calculus. Again, i take a page from the process algebra community, who were, whether they knew it or not, taking a page from Abramsky's domain theory in logical form. Here are some relevant references:

http://web.comlab.ox.ac.uk/oucl/work/samson.abramsky/dtlf.pdf

and

http://ctp.di.fct.unl.pt/~lcaires/papers/BehSpaObs.ps

The latter shows the application of a general technique of deriving a logic from term structure to the π-calculus. The former shows the origins of thinking about such techniques. In Namespace Logic: A Logic for a Reflective Higher-Order Calculus. (Trustworthy Global Computing, International Symposium, TGC 2005, Edinburgh, UK, April 7-9, 2005, Revised Selected Papers; Spring er sent me this link http://dx.doi.org/10.1007/11580850_19; or try http://www.springerlink.com/content/978-3-540-30007-6/ for the TGC publication), Matthias Radestock and i applied the same technique Caires does in his Behavioral and Spatial Observations paper but to a π-calculus with quotation, discovering a logic that allowed us to reason about names and name spaces.

In what follows below i simply apply the technique to generate a program logic for the λ-calculus with quotation that i presented in (http://lambda-the-ultimate.org/node/1930). Just as Howard follows Curry in the Curry-Howard isomorphism, you can bet that a type system follows from this logic.

In the sequel we let Λ(M) denote the set of terms generated by the following grammar

Likewise, we let Λ(^M^) denote the set of names generated by said grammar. Also, we use ≡ to denote the structural equivalence relation defined in (http://lambda-the-ultimate.org/node/1930). Now, we borrow another page from Caires and present simultaneously the syntax and semantics of our logic.

Discussion... first, i leave it as an exercise to the reader to add a greatest fix point formulae and its semantics to this presentation. You can crib Caires paper to get a nice clean extension. Next i submit, without proof, that pretty much all the freshness machinery coming out of Pitts and Gabbay can be captured within this framework.

Now, here's one of the practical applications that has been driving a lot of this work. Suppose that you had a database of programs. (E.g., oh, say source forge, or google code base.) Now, suppose you wanted to find a program not on the basis of what the code is called, or what the variable names were, but on the basis of what the code does. This logic gives the basis for a query engine in which the structure and dynamics of programs can be queried.

In a subsequent posting i will write down some interesting formulae. Let me close this posting by saying that all i am doing is applying a sequence of functors, the quotation functor, and then the logic generating functor. These functors -- being functors -- are preserving a certain structure, including the term structure. The sequence unveils the 'dynamics', the unfolding of the notion of computation, implicit in λ-calculus. Much of this can be seen as a working out of Christopher Alexander's ideas about structure preserving processes, as he describes in the Nature of Order.

I am a Ph.D. statistician (with no formal GP training) with a perfervid desire for upgrading "old" statistics,
which was formulated within the small-data setting of the day over 200 years ago, to accommodate today's big data via hybrid GP-statisitcs models.

Now, my question of long standing in my head without an answer, if you please.I was told several years ago by a University of Chicago assistant professor, who was on the board of doctoral students in GAs/GPs,
that the GA paradigm can be extended into the GP paradigm. Is this true?
If so, I would appreciate a path-of-least resistance reply from you: a reference, or a quick blurb from you.

thanks.
Bruce