Hi, I am trying to understand the concept of dependent types as described in Haskell literature (Hallgren 2001),(Hinze,Jeuring et al. 2006). I am particularly interested in understanding two flavours 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 I think that ascending levels of abstraction are important here: values - types - classes (Hallgren 2001). Here is a Haskell example of the use of DT: 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) I think that the intended semantics are: 1) Objects have names and can be compared for equality using these names. 2) Two objects are considered equal (identical) if they have the same name. 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. My questions are: Question 1: Is my understanding correct? Question 2: What flavour of DT is this does this example exhibit? Best regards, Pat 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.
On Fri, Oct 9, 2009 at 6:11 AM, pat browne
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)
This is a type-indexed type. On a modern GHC I would write it this way: class Named a where type Name a name :: a -> Name a instance (Named a, Eq (Name a)) => Eq a where o1 == o2 = name o1 == name o2 Although to be honest I wouldn't write it this way at all, because your Eq instance is too general (remember, constraints are not examined when doing typeclass resolution; you are not saying "every type 'a' that is an instance of Named with Eq (Name a) is also an instance of Eq", you are saying "EVERY type 'a' is an instance of Eq, and please add the additional constraints 'Eq (Name a)' and 'Named a'")
My questions are: Question 1: Is my understanding correct? Question 2: What flavour of DT is this does this example exhibit?
When you say "Dependent Types", what is usually meant is that types can depend on *values*; for example: data Vector :: Integer -> * -> * where Nil :: Vector 0 a Cons :: a -> Vector n a -> Vector (n+1) a Now you might write this function: zip :: forall a b. (n :: Integer) -> Vector n a -> Vector n b -> Vector n (a,b) zip 0 Nil Nil = Nil zip (n+1) (Cons x xs) (Cons y ys) = Cons (x,y) (zip n xs ys) Notice that the *type* Vector n a depends on the *value* of the argument 'n' passed in. Normally it is only the other way around; values are limited by what type they are. Here we have types being affected by some object's value! -- ryan
I'll see if I can't gloss over some of the stuff Ryan Ingram already covered. On Friday 09 October 2009 9:11:30 am pat browne wrote:
2) Types depending on types called parametric and type-indexed types
The above distinction in types (and values) depending on types has to do with operations beyond just said dependency. For instance: data List a = Nil | Cons a (List a) Is the definition involving types that depend on other types. And similarly: foo :: forall a. List (List a) foo = Cons Nil Nil is a value that depends on a type. In a language more explicit about type application, one might write: foo@a = Cons@(List a) Nil@a Nil@(List a) So far, these fall in the parametric category, but your example does not:
class Named object name | object -> name where name :: object -> name
Classes in H98 allow you to define non-parametric type->value dependence, and when extended with functional dependencies, or alternately, if we consider type families, we get non-parametric type->type dependence. The difference isn't in what things can depend on what other things, but in what operations are available on types. Specifically, type classes/families are like being able to do case analysis on types, so in the value case: class Foo a where bar :: [a] instance Foo Int where bar = [5] instance Foo Char where bar = "c" can be seen as similar to: bar@c = typecase c of Int -> [5] Char -> "c" And type families are similar on the type-level (it's less clear how functional dependencies fit in, but a one way a -> b is kind of like doing a type-level typecase on a to define b; more accurately you have multiple type parameters, but in each a-branch, b there is exactly one b-branch). Of course, this is an over-simplification, so take it with salt.
I am aware that dependent types can be used to express constraints on the size of lists and other collections.
Technically, you don't need dependent types for this, you just need type-level naturals. But dependent types (or some sufficiently fancy faking thereof) are nice in that you only need to define the naturals once, instead of at both the value and type levels.
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.
As Ryan remarked, this is not a value->type dependency. In the instance, you are defining equality for the type 'object' which determines the type 'name' in a type->type dependency. You're then defining equality on values of type 'object' via equality on values of type 'name', via the 'name' function. But that's just value->value dependency which every language of course has. GHC does have ways of faking dependent types, though, with GADTs. GADTs allow you to define data such that matching on constructors refines things in the type system. So, along with the mirroring mentioned above, you can manually set up a value->type dependency that acts like full-on dependent types. For naturals it looks like: -- type level naturals data Zero data Suc n -- value-level GADT indexed by the type-level naturals data Nat n where Zero :: Nat Zero Suc :: Nat n -> Nat (Suc n) -- existential wrapper data Natural where Wrap :: Nat n -> Natural Ryan's zip function would look like: zip :: forall a b n. Nat n -> Vector n a -> Vector n b -> Vector n (a,b) zip Zero Nil Nil = Nil zip (Suc n) (Cons x xs) (Cons y ys) = Cons (x,y) (zip n xs ys) although the 'Nat n' parameter is technically unnecessary in this case. But, in some other function: foo :: forall n. Nat n -> T foo Zero = {- we know type-level n = Zero here -} foo (Suc n) = {- we know type-level n = Suc m for some m here -} Of course, mirroring like the above is kind of a pain and only gets more so the more complex the things you want to mirror are (although this is how, for instance, ATS handles dependent types). There is a preprocessor, SHE, that automates this, though, and lets you write definitions that look like a full- on dependently typed language (among other things). Anyhow, I'll cease rambling for now. Cheers, -- Dan
Hi, I am attempting to explain an example of dependent types to computing practitioners who do not have any background in functional programming. My goal is to explain the example rather than implement or improve it. I have been told in previous postings that the approach below is a bit dated. Any comments on the correctness or otherwise would be appreciated. Regards, Pat ======================================================= Dependent Types (DT) The purpose of dependent types (DT) is to allow programmers to specify dependencies between the parameters of a multiple parameter class. DTs can be seen as a move towards more general purpose parametric type classes. DTs 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 DT 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 Eq instance 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. Dan Doel wrote:
I'll see if I can't gloss over some of the stuff Ryan Ingram already covered.
On Friday 09 October 2009 9:11:30 am pat browne wrote:
2) Types depending on types called parametric and type-indexed types
The above distinction in types (and values) depending on types has to do with operations beyond just said dependency. For instance:
data List a = Nil | Cons a (List a)
Is the definition involving types that depend on other types. And similarly:
foo :: forall a. List (List a) foo = Cons Nil Nil
is a value that depends on a type. In a language more explicit about type application, one might write:
foo@a = Cons@(List a) Nil@a Nil@(List a)
So far, these fall in the parametric category, but your example does not:
class Named object name | object -> name where name :: object -> name
Classes in H98 allow you to define non-parametric type->value dependence, and when extended with functional dependencies, or alternately, if we consider type families, we get non-parametric type->type dependence. The difference isn't in what things can depend on what other things, but in what operations are available on types. Specifically, type classes/families are like being able to do case analysis on types, so in the value case:
class Foo a where bar :: [a]
instance Foo Int where bar = [5]
instance Foo Char where bar = "c"
can be seen as similar to:
bar@c = typecase c of Int -> [5] Char -> "c"
And type families are similar on the type-level (it's less clear how functional dependencies fit in, but a one way a -> b is kind of like doing a type-level typecase on a to define b; more accurately you have multiple type parameters, but in each a-branch, b there is exactly one b-branch). Of course, this is an over-simplification, so take it with salt.
I am aware that dependent types can be used to express constraints on the size of lists and other collections.
Technically, you don't need dependent types for this, you just need type-level naturals. But dependent types (or some sufficiently fancy faking thereof) are nice in that you only need to define the naturals once, instead of at both the value and type levels.
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.
As Ryan remarked, this is not a value->type dependency. In the instance, you are defining equality for the type 'object' which determines the type 'name' in a type->type dependency. You're then defining equality on values of type 'object' via equality on values of type 'name', via the 'name' function. But that's just value->value dependency which every language of course has.
GHC does have ways of faking dependent types, though, with GADTs. GADTs allow you to define data such that matching on constructors refines things in the type system. So, along with the mirroring mentioned above, you can manually set up a value->type dependency that acts like full-on dependent types. For naturals it looks like:
-- type level naturals data Zero data Suc n
-- value-level GADT indexed by the type-level naturals data Nat n where Zero :: Nat Zero Suc :: Nat n -> Nat (Suc n)
-- existential wrapper data Natural where Wrap :: Nat n -> Natural
Ryan's zip function would look like:
zip :: forall a b n. Nat n -> Vector n a -> Vector n b -> Vector n (a,b) zip Zero Nil Nil = Nil zip (Suc n) (Cons x xs) (Cons y ys) = Cons (x,y) (zip n xs ys)
although the 'Nat n' parameter is technically unnecessary in this case. But, in some other function:
foo :: forall n. Nat n -> T foo Zero = {- we know type-level n = Zero here -} foo (Suc n) = {- we know type-level n = Suc m for some m here -}
Of course, mirroring like the above is kind of a pain and only gets more so the more complex the things you want to mirror are (although this is how, for instance, ATS handles dependent types). There is a preprocessor, SHE, that automates this, though, and lets you write definitions that look like a full- on dependently typed language (among other things).
Anyhow, I'll cease rambling for now.
Cheers,
-- Dan
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
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Hi Pat, you might be interested in Agda [1] and the tutorial "Dependently Typed Programming in Agda" [2]. I'm just reading the tutorial and it helps me a lot with understanding the concept. Also if you'd like to have a deeper understanding of the underlying theory, I'd suggest reading Barendregt's "Lambda Calculi with Types" [3]. Best regards, Petr [1] http://wiki.portal.chalmers.se/agda/ [2] http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf [3] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.4391 and ftp://ftp.cs.kun.nl/pub/CompMath.Found/HBKJ.ps.Z On Fri, Oct 09, 2009 at 02:11:30PM +0100, pat browne wrote:
Hi, I am trying to understand the concept of dependent types as described in Haskell literature (Hallgren 2001),(Hinze,Jeuring et al. 2006). I am particularly interested in understanding two flavours 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
I think that ascending levels of abstraction are important here: values - types - classes (Hallgren 2001). Here is a Haskell example of the use of DT:
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)
I think that the intended semantics are: 1) Objects have names and can be compared for equality using these names. 2) Two objects are considered equal (identical) if they have the same name. 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.
My questions are: Question 1: Is my understanding correct? Question 2: What flavour of DT is this does this example exhibit?
Best regards, Pat
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.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Petr, Thanks for the links. My research involves the study of current algebraic specification and programming languages. I have posted some very general and abstract style questions in order to get a better feel of the individual languages. I do not wish to become highly proficient in each language, so any links that speed up my research are much appreciated. Thanks again, Pat Petr Pudlak wrote:
Hi Pat,
you might be interested in Agda [1] and the tutorial "Dependently Typed Programming in Agda" [2]. I'm just reading the tutorial and it helps me a lot with understanding the concept.
Also if you'd like to have a deeper understanding of the underlying theory, I'd suggest reading Barendregt's "Lambda Calculi with Types" [3].
Best regards, Petr
[1] http://wiki.portal.chalmers.se/agda/ [2] http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf [3] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.4391 and ftp://ftp.cs.kun.nl/pub/CompMath.Found/HBKJ.ps.Z
On Fri, Oct 09, 2009 at 02:11:30PM +0100, pat browne wrote:
Hi, I am trying to understand the concept of dependent types as described in Haskell literature (Hallgren 2001),(Hinze,Jeuring et al. 2006). I am particularly interested in understanding two flavours 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
I think that ascending levels of abstraction are important here: values - types - classes (Hallgren 2001). Here is a Haskell example of the use of DT:
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)
I think that the intended semantics are: 1) Objects have names and can be compared for equality using these names. 2) Two objects are considered equal (identical) if they have the same name. 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.
My questions are: Question 1: Is my understanding correct? Question 2: What flavour of DT is this does this example exhibit?
Best regards, Pat
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.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (6)
-
Benjamin Franksen -
Dan Doel -
pat browne -
pbrowne
-
Petr Pudlak -
Ryan Ingram