Hi Ramana, >Perhaps it would make more sense to ask people who are using rich type >systems what their motivations are :) >(On this list it's probably mostly people who are satisfied with simple >type theory.)
One can do everything with anything. So dependent tpes certainly are not _needed_ for formalization. But dependent types _are_ very convenient. I know them both from Coq and from Mizar. In Mizar the foundations are untyped ZF-style set theory (Josef Urban's PhD thesis is about cooking away all the syntactic sugar), so you don't need an "an enormously complex logic" (Mario's words) to get dependent types. Examples of types that to me seem dependent in a natural way are, in mathematics: element of the set X element of the carrier of the algebraic structure X vector space of dimension n normal subgroup of group G field of characteristic p field extension of field K simplicial k-complex morphism from A to B in a category and in (theoretical) computer science: array of length n integer of signedness s and size n machine program of processor architecture P C program of implementation I normal form of term t under some reduction relation term of type A in a typed system or in mathematical logic: proposition over a signature S proof of proposition A Etcetera, etcetera. The last actually _also_ has the signature S as an argument, but it is "hidden" (implicit) because it can be inferred from the type of A, so does not need to be written. These implicit arguments are quite powerful. For example, when working in group theory, you can write x + y, but actually it will be a ternary operation, with the group the third argument that can be inferred from the type of x and y. I know that John Harrison has a hack where he uses type variables to simulate natural numbers, and you get _something_ like dependent types in HOL that way. But that really only goes so far. Now various of these types are sometimes in a natural way empty (for example the type "normal form of term t", when t does not have a normal form), which makes it so irritating that Mizar doesn't allow for empty types. Without dependent arguments, not allowing for empty types is not a big deal (like in HOL), but once you ahve dependent types you really also have to allow for types being empty. Even when you don't care at all (like I do, well maybe :-)) for the Curry-Howard isomorphism. Freek ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
