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

[pat browne]

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 at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe