[Haskell-cafe] Re: Approaches to dependent types (DT)

[pbrowne]

Ben,
I have added your input. Thanks for putting me right.
Pat


Functional Dependencies
The purpose of functional dependencies (FD) is to allow programmers to
specify dependencies between the parameters of a multiple parameter
class. FD reduces the number of possible instances, or models of a
class. Note, the notion of FD is distinct from the concept of 'Dependent
types', where the result type (of a function) can depend on argument values.

FD are declared in a class header, where the type of one class
parameter is declared to depend on another class parameter. Consider the
following example:

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

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

The first part of the class definition Named takes two type variables as
parameters; namely object and name. We say, that object determines name
or alternatively that name is determined by object. This is denoted in
the second part of the class header (i.e. | object -> name). With DTs,
the dependent type depends on values of the determining type.  Hence, a
FD involves a relation between Haskell’s value-level and the type-level
(or type system). The Named class contains the signature, but not the
definition, of one function called namef. Note, the in the definition of
namef, the argument and return type (object -> name) are textually
identical to that occurring in the class header, however the semantic is
that of function definition rather that of type dependency.
In the instance declaration, the part before the => is called the
context, while the part after the => is called the head of the instance
declaration. The context contains one or more class assertions, which is
a list of classes each with their respective type variables, asserting
that a type variable is a parameter of a particular class. The context
for the above example includes two previously defined classes. The Eq
class is defined in the Haskell prelude and our user defined Named
class.  The instance asserts:
If  (type of name is an instance of the Eq class) and
 (type pair (object, name) is an instance of  Named)  then
                                      object is an instance of Eq
The new Eq instance defined is quite general, it asserts that every type
object is
an instance of the Eq class.  It does not say that every type object
that is an instance of Named is also an instance of Eq.
Now we consider the definition of equality (==) for the type object in
the instance body. Initially, the definition determines the type name in
a type->type dependency (e.g. via the function call namef object1). When
the two names have been calculated the function uses this information to
define equality on values of type  object via equality on values of type
name.



Benjamin Franksen wrote:
> pbrowne wrote:
>> Dependent Types (DT)
>> The purpose of dependent types (DT) is to allow programmers to specify
>> dependencies between the parameters of a multiple parameter class.  
> 
> 'Dependent type' means result type (of a function) can depend on argument 
> values. This is not (directly) supported in Haskell.
> 
> What you are talking about is called 'functional dependencies', not 
> 'dependent types'. Sometimes abbreviated as 'fundeps'.
> 
>> DTs
>> can be seen as a move towards more general purpose parametric type
>> classes. 
> 
> This is at least misleading, as adding a functional dependency does not make 
> the class more general, but more special, as it reduces the number of 
> possible instances.
> 
> Cheers
> Ben
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe