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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe