Lambda the Ultimate

In the spirit of the What Are The Resolved Debates in General Purpose Language Design? topic, I would be interested in hearing your opinion on the specific Syntax Design problem. In designing a new syntax for a programming language, what are the decisions that are objectively good (or bad) ?

Most syntaxic questions are rather subjective (for example, 'CamelCase' or 'with_underscores' identifiers ?), but I think that some can be answered definitely with a convincing argumentation.

Here is one example : recursive scoping should always be optional and explicit. Recursive scoping is when a defined identifier scope is active at the definition site as well as at the usage site. In Haskell, term definitions have recursive scoping by default, while OCaml doesn't (there is a let .. and a let rec ... syntax). It allows for useful programming idioms such as let x = sanitize x in ... or let (token, i) = parse i. Haskell programmers would sometimes benefit from such a possibility, as can be seen here and here. type definitions are implicitely recursive in OCaml and this is also a pain.

Example of debates that are probably not resolved (yet ?) :

• identation-sensitive syntax
• open (if .. else ..) or closed (if .. elif .. else .. end) conditional statements

Do you know of ressources discussing such syntaxic issues in a general way applicable to numerous/all (textual) programming languages ?

In Lisps, where definitions, expressions, and syntax transformers can be mixed freely in a block of code, the semantics of environments become a bit complicated, I think.

R6RS's expansion process is the best and most clearly described semantics for such blocks that I know.

In effect, a block of code is transformed into a letrec*, with dummy bindings for expressions that are between definitions. Furthermore, the syntax transformation of the right-hand sides is delayed until all definitions in the block have been seen.

This seems sensible, but I wonder if anyone has pointers, information, or rationale for R6RS's and other possible approaches to the semantics of such environments?

Thanks

Approaches to dependent types(DT)

Introduction
I am trying to tease out the differences and similarities between concept of dependent types as described by Goguen (Goguen 1991) and as described in Haskell literature (Hallgren 2001),(Hinze,Jeuring et al. 2006).
At the theoretical level I could compare type theory (Thompson 1991)and the theory of institutions (TOI) (Goguen and Burstall 1992). But this is way beyond my expertise. I would like to keep the comparison at a reasonably practical level but at the same time avoid a low level language-to-language comparison. I use CafeOBJ as an example of an institution based language. Intuitively I say that CafeOBJ is a specification language that allows some programming while Haskell is a programming that allows some specification by using type class and type inference. The CafeOBJ sort roughly corresponds to the Haskell type. It is convenient to have high level concepts that describe both approaches. I use the following slogans and levels of abstraction to distinguish Haskell (type theory)and CafeOBJ(istitutions) approaches.

Slogans
Haskell: types as theorems and programs as proof
CafeOBJ: types as theories and truth is invariant under change of notation

Ascending Levels of abstraction
Haskell: values - types - classes (Hallgren 2001)
CafeOBJ: data elements - data set - concrete algebra - abstract algebra (Goguen 1991)

Dependent types in Haskell
==========================
I am particularly interested in understanding two types of dependency mentioned by
Hinze et al:
1) Types depending on values called dependent types
2) Types depending on types called parametric and type-indexed types

Here is a Haskell example of the use of DT from (Raubal and Kuhn 2004).

class Named object name | object -> name where
name :: object -> name

instance (Eq name, Named object name) => Eq object where
object1 == object2 = (name object1) == (name object2)

The intended semantics are:
1) Objects have names (or other identifiers) and can be compared for
equality using these names.
2) Two objects are considered equal (identical) if they have the same
identifier.
3) The type of a name depends on the type of the object, which gets
expressed as a type dependency (object -> name).

I am not sure about the last semantic it might be interpreted as "the named object depends on..".
This may indicate a flaw in my understanding of DT.
I am aware that dependent types can be used to express constraints on the size of lists and other collections. My understanding of Haskell's functional dependency is that | object -> name indicates that fixing the type object should fix the type name (equivalently we could say that type name depends on type object). The class definition seems to show a *type-to-type* dependency (object to name), while the instance definition shows how a name value is used to define equality for objects which could be interpreted as a *value-to-type* dependency (name to object) in the opposite direction to that of the class.

============================================================
Question 1: Is my understanding correct?
Question 2: What type of DT is this does this example exhibit?
==============================================================

My attempt at dependent types in CafeOBJ
================================================
Joseph Goguen also uses the term dependent type in his Types as Theories paper (Goguen 1991).
I will postpone a detailed discussion of Goguen's excellent paper (it needs more careful study).
The module NAMEDOBJECT is my first stab at converting the Haskell definitions above into CafeOBJ module.
When the module is opened with actual parameters the variable n1 of type Elt.name is replaced by the actual imported sort (type) that will be used to define the type equality for the actual sort the will be substituted for Elt.object. The TRIV module is used as a formal parameter, Elt is the only sort in the TRIV module and represents any set of elements. TRIV can be considered the most abstract module in CafeOBJ, it has just one sort Elt. Hence almost any more complex sort can replace it as long as it has one sort (type). Here is the definition of TRIV.
mod* TRIV
{
[ Elt ]
}

Note CafeOBJ modules are parameterized by other modules (not type variables as in Haskell classes)
Here TRIV module being used a parameter (or interface theory) to the NAMEDOBJECT module.

mod! NAMEDOBJECT(object :: TRIV, name :: TRIV) {
op name__ : Elt.object Elt.name -> Elt.name -- get name
vars o1 o2 : Elt.object
var n1 : Elt.name
eq name o1 n1 = n1 .
eq (o1 == o2) = if (name o1 n1 == name o2 n1) then true else false fi .}

We can now open the module with any appropriate types
open NAMEDOBJECT(INT,QID) .

In the system generated module replaced sorts can be clearly seen.
module NAMEDOBJECT(object { ** opening
imports {
protecting (INT)
protecting (QID)
}
signature {
op o _ _ : Int Id -> Int { strat: (0 1 2) prec: 41 }
op n _ _ : Int Id -> Id { strat: (0 1 2) prec: 41 }
}
axioms {
eq (o o1:Int n1:Id) = o1 .
eq (n o1:Int n1:Id) = n1 .
eq (o1:Int == o2:Int) = (if ((n o1 n1:Id) == (n o2 n1)) then true else false fi) . }}

Some points for comparison:
The name type does not really depend on the object.
It seems that they both fit the specification of NAMEDOBJECT.
My first impression is there is no type inference in the Haskell sense.

I can see my first attempt does not quite match the semantics of Haskell version.
I would be grateful if you have any advice on:
1) how to improve my translation attempt and
2) how to develop a better understanding of Haskell DT(particular the relation between value and type).

Best regards,
Pat

Goguen, J. (1991). Types as Theories. Topology and Category in Computer
Science. G. M. Reed, A. W. Roscoe and R. F. Wachter, Oxford University
Press: 357-390.

Goguen, J. and R. Burstall (1992). "Institutions: abstract model theory for specification and programming." Journal of the ACM 39(1): 95-146. See http://en.wikipedia.org/wiki/Institution_(computer_science)

Hallgren, T. (2001). Fun with Functional Dependencies. In the
Proceedings of the Joint CS/CE Winter Meeting, Varberg, Sweden, January
2001.

Hinze, R., J. Jeuring, et al. (2006). Comparing Approaches to Generic
Programming in Haskell. Datatype-generic programming: international
spring school, SSDGP 2006.

Raubal, M. and W. Kuhn (2004). "Ontology-Based Task Simulation." Spatial
Cognition & Computation 4(1): 15-37.

Thompson, S. (1991). Type Theory and Functional Programming, Addison-Wesley.