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.