Lambda the Ultimate

First appologize for my poor English.:)So,I just write more codes.

I'v found a new way of reusing codes:

Question:
there are three properties: Prop1，Prop2，Prop3.they all have a member named "Value".

Prop1.Value:=1; //Prop1 is defined as integer type.
Prop2.Value:=2.345; //Prop2 is defined as float type.
Prop3.Value:=’abc’; //Prop3 is defined as string type.

How to write a function return all these propX's value?
We can write like this:

function GetPropertyValueofProp1: Integer;
begin
Result：=Prop1.Value;
end.

function GetPropertyValueofProp2: double;
begin
Result=Prop2.Value;
end.

function GetPropertyValueofProp3: string;
begin
Result=Prop3.Value;
end.

these three functions are very similar,can we write one function to deal with it?

In my new programming language "Zero",it is OK!
We can write a function like this:

function GetPropertyValue(Ψprop): Ψtype;
begin
result:= Ψprop.Value;
end

So strange!Can it work?How to use it?Can the compiler of the language deal with it?

Zero language has an IDE named "Amoeba".Through the syntax of the function analysis, Amoeba knows:
1 Ψprop contains a member named "Value".
2 Ψtype is a type.
3 The type of Ψprop.Value is same as Ψtype.

so,when we write the function in IDE:

var m1: Integer;
m1:=GetPropertyValue (____);

There is a blank we should fill.Amoeba's Code assist will give the message:
[ Prop1 ]

It means there is only one selection we can fill.Why?

Because m1 is integer type,and each side of ":=" has the same type,"Amoeba" knows it.

if the code is like this:

var m1;
m1:=GetPropertyValue (____);

Amoeba's Code assist will give the message:
[Prop1,Prop2,Prop3]

Why?because Amoeba don't know m1's type.So there are 3 selections.
The most intresting thing is,when we fill the blank with "Prop2",
What will happen?

Now m1 has a "float" type!

Let's explain the new way of reusing codes,the rule is:

If we found similar codes,write it directly,if something is
undetermined，represent it with Ψ.The Amoeba IDE always knows what do you want.I know STL can do something similar,but Amoeba is more powerful and friendly for users.

Some time ago I have seen an article reference on LtU that discussed representing cyclic graphs using purely functional data structures. The graph structure was something like flow graph or state machine.

The article discussed switch from implementation based on mutable variables to purely functional version, and the thesis of article was that the authors lived more happily with purely functional version afterwards.

I was unable to locate article using search (too many unrelated results), if somewhat remember the article or at least its title, please give me a reference.

Greetings LTU.

I am very new to type theory, taking an independent study in it at my university as my interests seem to point in this direction. However, as an independent study at a university where no one has a real specialization in the subject, there are some basics that I am struggling with. Are there any good forums that would be recommended for someone of my level where I could post questions that I just can't figure out and get some guidance? Thank you in advance.

I love RPN calculators and have been experimenting with how it may be possible to extend the RPN stack style into a structured programming language. Ambi is the result. Here is Ambi for the factorial function and an invocation:

function; ! ;
seq ; import $n = ;
ifelse;
$n 1 eq;
1 export;
$n 1 - ! $n * export;

5 ! .;

(The 'import' operator pops the top stack item from the calling context and pushed it onto the expression's stack. 'export' is the converse pushing the top of the expression's stack back out into the calling context's stack.)

Notice that the program is written using Polish (prefix) notation without any brackets and individual expressions are written in Reverse Polish (postfix) notation. Actually, Ambi doesn't care whether the programmer writes the program (and individual expressions) in prefix or postfix notation. Here is the exact same program written in postfix.

import $n = ;
$n 1 - ! $n * export;
1 export;
$n 1 eq;
ifelse; seq;
! ; function

Ambi is an open source language and has been implemented in browser-based Javascript and an interpreter and documentation lives at http://www.davidpratten.com/ambi There are lots of example programs there that can be loaded into the interpreter just by clicking on them.

Ambi owes a debt to Forth, RPL and to CAT. CAT (and earlier) JOY elected to make the composition operator implicit, whereas in Ambi it is made explicit in the 'seq' operator.

Your observations, suggestions, and/or critique are welcome.

David

I have a passion for Programming Language Design; designing compilers, languages and dreaming up functional code; I just finished undergraduate studies from Purdue University (BS: Computer Engineering) and would like to pursue the above for further studies...which schools and deptt. that humble readers of LtU may know of, would you recommend? It doesn't have to be in US necessarily but that helps...just a bit more on myself; so far, I've not done anything ingenious; just followed standard compiler texts and replicated their code to understand what's going on...in this way, I've implemented compilers for very simple subsets of Java and C. There's obviously so much to do! PS: planning to start with graduate studies in Fall '10 (currently working as .NET developer with an IT Consultancy). Any help/advice greatly appreciated! LtU rocks! (and "yes", I DO know what a y-combinator is! (yay!)).

(PS: I see there is a "Course">""Graduate Programs in Program Design" Link in this blog but I am seeking a more forthcoming response; of course I will scour through all the listings in detail but where is the action happening RIGHT NOW? Which schools? Under which professors?

THANKS!

Shubham Harnal.

There are relatively few language specifications out there which incorporate a formal statement of semantics and typing rules. Of those that do, the one that I'm most familiar with (ML) uses a fairly hard to read notation.

We're at the point where we want to incorporate such a statement into the BitC specification, and I'ld appreciate pointers, inputs, and suggestions on how we might express these things with the greatest clarity and precision. It seems to me, naively, that we need to specify how the full language syntax maps (syntactically) to a canonicalized core syntax, and then specify the semantics and typing rules for that core. At the moment, I'm attracted to the notation used by Pierce's book (and of course by others). I'm willing to sacrifice textual compactness for clarity. On the other hand, the idea of formalizing directly in Coq has its appeal.

Are there examples of specifications out there that we should look at as potential exemplars? If so, why are they exemplars? What makes them good. Conversely, are there examples out there of approaches to avoid, and why?

Aside: this isn't the right forum for an extended discussion of formalizing BitC in particular, but if you would like to participate in that process, please do come join the appropriate mailing list.

Are there parser DSLs which allow you to 'nicely' specify error handling? It seems natural with, say, parser combinators, though something that is otherwise more akin to LL(1) would be more interesting.

The context is that some of the most common languages are generally thought of as LL(1), CFGs, etc., yet, in reality, their informal specifications allow some forms of erroneous input and actually define how to handle them. This means they're not really erroneous, but pockets of complication that should be somewhat uniformly handled in an isolated manner.

(seen via http://catless.ncl.ac.uk/Risks/25.51.html#subj9.1, i didn't find it searching on ltu yet)

at qcon, london:

Abstract: I call it my billion-dollar mistake. It was the invention of the null reference in 1965. At that time, I was designing the first comprehensive type system for references in an object oriented language (ALGOL W). My goal was to ensure that all use of references should be absolutely safe, with checking performed automatically by the compiler. But I couldn't resist the temptation to put in a null reference, simply because it was so easy to implement. This has led to innumerable errors, vulnerabilities, and system crashes, which have probably caused a billion dollars of pain and damage in the last forty years. In recent years, a number of program analysers like PREfix and PREfast in Microsoft have been used to check references, and give warnings if there is a risk they may be non-null. More recent programming languages like Spec# have introduced declarations for non-null references. This is the solution, which I rejected in 1965.

I'm implementing a language that supports nested functions with closure semantics, i.e.

def func(x:int) returns (int):int
{
   return def nested(y:int) returns int 
          { x*y; }
}

Now, to simplify the closure implementation, I only allow one nesting level. Is this overly restrictive? What does other languages do?

I haven't come across a real-life use-case for multiple nesting levels.

Any opinions / counter examples would be greatly appreciated.

Thanks.
-s

This paper [pdf] describes an efficient interpreter for lazy functional languages like Haskell and Clean. The interpreter is based on the elimination of algebraic data types and pattern-based function definitions by mapping them to functions using a new efficient variant of the Church encoding. The transformation is simple and yields concise code.