Lambda the Ultimate

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.

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

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 ?

Ever wanted to learn a little Prolog? Want to learn what it's good for? Join us at the next FringeDC Meeting. Afterwards, we'll stop at a nearby restaurant for some food and to discuss programming.

The meeting will be held at the Clark&Parsia offices in downtown DC near the Convention Center(clarkparsia.com/contact)

FringeDC is a group in Washington DC interested in fringe programming languages (Lisp, Haskell, Erlang, Prolog, etc.) Anyone is welcome to join our meetings!

www.lisperati.com/fringedc.html

I'm on a campaign, I'm joining a revolution, and it's guiding maxim is this...

"Simplicity is the Price of Reliability, a price which I'm now fully prepared to pay."

The full quote comes from The Emperor's Old Clothes C.A.R. Hoare 1980 ACM Turing Award Lecture

"The price of reliability is the pursuit of the utmost simplicity. It is the price the very rich find most hard to pay."

While more features go into a language, in particular threading, I cannot write reliable programs, since the language compiler / interpretor itself becomes ever more complex.

So I'm on a hunt for the some other language to be my prime tool.... and Threading is at the top of my list of "features not to have".

I've learnt my limitations... unlikely most programmers, I know I'm not smart enough to code reliably in C / C++ like languages. (I didn't say I'm less smart than most programmers, merely that unlike most programmers I know I'm not smart enough.)

The code implementing Rubies interpretor is, ahh, um, threaded through with support for threading...

Common Lisp has the simplicity of Syntax but is a horrendous sprawl of semantics.

Scheme is near the top of my list, but I suspect a touch more expressiveness in semantics may make large programs simpler.

Scala appeals... but building it ontop of JVM strikes me as a very very bad start.

I'm begging for suggestions.

I've been reading about the Lambda cube type scheme of Henk Barendregt and found it interesting if a little obscure. Does anyone know of any languages that implement the "full cube" (the 8th corner of the cube). I'm familiar with Haskell but I don't think it has dependent types (axis 2 IIRC).

Not really the PL-applicable sort of topology, but I think it will be interest to a fair few folks here: there's a PDF scan of James Munkres (2000) Topology available.

Postscript: Not anymore. I guess it was not a legitimate distribution of the text.

Postscript #2: Or maybe it does still, for some...

I am reading The language instinct from Steven Pinker. Some of the examples he has are very familiar to compiler construction.

Shift/Reduce conflictis a conflict in LALR grammars (most programming languages) where in the parser has to decide between shifting a new token for a rule or reducing the rule. Quoting Stephen C. Johnson from the YACC paper

As an example of the power of disambiguating rules, consider a fragment from a programming language involving an ``if-then-else'' construction:

    
   stat  :  IF  '('  cond  ')'  stat
         |  IF  '(' cond ')'  stat  ELSE  stat ;

These two rules form an ambiguous construction, since input of the form

   IF  ( C1 )  IF  ( C2 )  S1 ELSE  S2

can be structured according to these rules in two ways:

   IF  ( C1 )  {
                IF  ( C2 )  S1
               }
   ELSE S2

or

   IF  ( C1 )  {
                IF  ( C2 )  S1
                ELSE  S2
               }

The second interpretation is the one given in most programming languages having this construct.

That is during a shift/reduce conflict, LALR parsers chose shift over reduce, implying that clauses are always associated with the innermost clause.

On the human side of the equation, Steven Pinker talks about Chomsky's classic illustration of turning a declarative sentence into a question

         A unicorn is in the garden
   -> Is a unicorn    in the garden?

This is done by taking the auxiliary "is" and moving it. However, this is not a simple move as illustrated in the below case

            A unicorn that is eating a flower is in the garden
   ->    Is a unicorn that is eating a flower    in the garden?

Chomsky argues that our mental algorithm does not pick words by their linear positions, but does so by grouping it into phrases, implying that during a conflict the mind chooses entire units together.

Does this mean that the designers of LALR were goaded by their mintal algorithm to chose shift instead of reduce? Or does this mean that language is an algorithm (albeit more powerful than any parser) that is wired into our brain - and evolution chose shift over reduce because that is the easier one to implement?

Also at here

...a domain specific language for simulating football. ... We have used Soccer-Fun in teaching during the past four years. We have also experience in using Soccer-Fun for pupils in secondary education. ... It engages students to problem solving with functional programming because it allows them to compete at several disciplines: the best performing football team can become champion of a tournament; the best written code can be awarded with a prize; students can be judged on the algorithms used. This enables every student to participate and perform at her favourite skill. ... It can be implemented in any functional programming language that supports some kind of windowing toolkit.

Teaching Functional Programming with Soccer-Fun (pdf)

Peter A. H. Petersen has written two weblog posts on abstraction and security:

• Abstraction -- Friend or Foe?, and
• Abstraction and Trade-offs: The Devil You Know.

The points he makes echo a theme dear to my heart: abstractions offer the programmer compositionality of construction when creating their programs and systems, but that notion of compositionality does not match all of the properties one needs to ensure that a system is secure. Cf. slogan #2, from my story The irreducible physicality of security properties:
 Security is non-modular: Programming languages and software engineering practices can ensure that software possesses properties helpful to security, but the properties are only meaningful in the context of a strategy to ensure a computer system satisfies its security policy;

Postscript — Before someone mentions it, Joel Spolsky wrote something quite relevant: The Law of Leaky Abstractions