The Artima Developer Community
Sponsored Link

Weblogs Forum
Searching for a Definition of Type

8 replies on 1 page. Most recent reply: Sep 8, 2006 8:07 PM by Isaac Gouy

Welcome Guest
  Sign In

Go back to the topic listing  Back to Topic List Click to reply to this topic  Reply to this Topic Click to search messages in this forum  Search Forum Click for a threaded view of the topic  Threaded View   
Previous Topic   Next Topic
Flat View: This topic has 8 replies on 1 page
Christopher Diggins

Posts: 1215
Nickname: cdiggins
Registered: Feb, 2004

Searching for a Definition of Type (View in Weblogs)
Posted: Sep 8, 2006 12:04 PM
Reply to this message Reply
Summary
My most recent post has sparked some debate. I thought I'd put my money where my mouth is and try to define type.
Advertisement
In my latest blog post Authors and Computer Scientists Scared of Definitions? I use the example of the lack of a definition of type in Pierce's book Types and Programming Languages as a source of frustration. As is traditional with online debates I was asked to define type myself (I wonder if film critics are ever asked to make films?).

At http://plato.stanford.edu/entries/type-theory we can get a great primer on type theory from the Stanford Encyclopedia of Philosophy. There is actually a rigorous definitions of type given, which I summarize as follows:

A type is a classification of individuals, propositions, and relations. There are two basic types: i (the type of individuals) and o (the type of propositions). If A1,...,An are types then (A1,...,An) is the type of the n-ary relation over objects of the respective types. Types are used to filter non-legal relations and propositions.
To understand this in simpler terms, realize that a function is a binary relation. So a function from the type T to the type U has the type (T, U). This is written using more modern notation as T->U.

Feel free to discuss!


John Cowan

Posts: 36
Nickname: johnwcowan
Registered: Jul, 2006

Re: Searching for a Definition of Type Posted: Sep 8, 2006 1:59 PM
Reply to this message Reply
I drive a stake in the ground thus:

A type is a named set of values, where a name is a string over some finite alphabet such as Unicode.

Note that this says nothing about nominal vs. structural typing: "a structure consisting of an integer named 'x' and an integer named 'y'" is just as good a type name as "Point".

Ensuring that all types have names makes sure that there are only an enumerably infinite number of types, since there are only an enumerably infinite number of names.

James Watson

Posts: 2024
Nickname: watson
Registered: Sep, 2005

Re: Searching for a Definition of Type Posted: Sep 8, 2006 2:34 PM
Reply to this message Reply
Probably flawed but this is what I am thinking (specific to programming languages)

A type is a specific classification of expression results.

James Watson

Posts: 2024
Nickname: watson
Registered: Sep, 2005

Re: Searching for a Definition of Type Posted: Sep 8, 2006 2:35 PM
Reply to this message Reply
> A type is a named set of values, where a name is a string
> over some finite alphabet such as Unicode.

Does a type need to be a value? At least conceptually, this seems too narrow. I don't think of functions as values but many languages have a function type.

James Watson

Posts: 2024
Nickname: watson
Registered: Sep, 2005

Re: Searching for a Definition of Type Posted: Sep 8, 2006 2:36 PM
Reply to this message Reply
> > A type is a named set of values, where a name is a
> string
> > over some finite alphabet such as Unicode.
>
> Does a type need to be a value? At least conceptually,
> this seems too narrow. I don't think of functions as
> values but many languages have a function type.

I meant, does a member of a type need to be a value?

Kay Schluehr

Posts: 302
Nickname: schluehk
Registered: Jan, 2005

Re: Searching for a Definition of Type Posted: Sep 8, 2006 3:32 PM
Reply to this message Reply
You might have noticed that the idea of "types" originated from correcting the naive notion of sets ( please also correct the link to the encyclopedia article! ). Instead of defining types intensionally they are defined formally as a filter for ill typed set expressions. Hence they do not simply classify entities ( that's what sets are for ) but they are used to express which terms are created by following certain rules ( type system ). My understanding of types in programming languages is that they constitute a refinement of syntax by semantics. Expressions that are otherwise syntactically correct can be sorted out because they lead to computations that get stuck. "Stuckness" is a part of the ideology of type theorists. Instead of becoming stuck a programmer can accept certain type faults and find meaningfull continuations within the catch-clause of the exception handler - I remember vaguely a polemics by Douglas Hofstadter in GEB about type theory as a desparate manner to lock intelligent beings into the rules of non-reflective formal systems. It takes no wonder that Hofstadter strongly advocated Lisp/Scheme. These days we might be more fascinated by using type expressions as expressions for defining invariants and for purpose of pattern matching.

Max Lybbert

Posts: 314
Nickname: mlybbert
Registered: Apr, 2005

Re: Searching for a Definition of Type Posted: Sep 8, 2006 4:23 PM
Reply to this message Reply
> > A type is a named set of values, where a name is a string over some finite alphabet such as Unicode.

> Does a type need to be a value?

I actually liked the definition of a named set of values, although some C++ template metaprogramming techniques create new types that don't do anything other than tell the compiler things (like with CRTP: http://en.wikipedia.org/wiki/Curiously_recurring_template_pattern ). I guess you could fudge and say that, as needed, the value might be "null" orthe value may not be contained in the implementation of the type, but rather be out-of-band (that is, the existence of the type in a particular situation is the important information).

Christopher Diggins

Posts: 1215
Nickname: cdiggins
Registered: Feb, 2004

Re: Searching for a Definition of Type Posted: Sep 8, 2006 5:28 PM
Reply to this message Reply
> You might have noticed that the idea of "types" originated
> from correcting the naive notion of sets ( please also
> correct the link to the encyclopedia article! ). Instead
> of defining types intensionally they are defined formally
> as a filter for ill typed set expressions.

You are right, this is a very pertinent piece of information that should be included in the definition. I have now added "Types are used to filter non-legal relations and propositions.".

Thanks for pointing that out to me.

Isaac Gouy

Posts: 527
Nickname: igouy
Registered: Jul, 2003

Searching for a reason to search for a definition Posted: Sep 8, 2006 8:07 PM
Reply to this message Reply
...I use the example of the lack of a definition of type in Pierce's book "Types and Programming Languages" as a source of frustration. As is traditional with online debates I was asked to define type myself (I wonder if film critics are ever asked to make films?).

If all a film critic had to say about "An Inconvenient Truth" was that the film maker hadn't defined "Inconvenient", we wouldn't ask them to make films and we wouldn't bother reading their film criticism :-)

afaict Nothing in your original posting indicated what difficulty the lack of a definition for "Types" caused you in understanding the book. If the lack of definition did indeed cause difficulty then you might provide that example to the author so he can consider the suggestion.

otoh If you simply wish to have a definition of "Types" and were disappointed that the book didn't contain one, maybe you should have checked if it included a glossary before forking-out the $70.

Flat View: This topic has 8 replies on 1 page
Topic: Searching for a Definition of Type Previous Topic   Next Topic Topic: Signs of the Next Paradigm Shift: Part I


Sponsored Links



Google
  Web Artima.com   

Copyright © 1996-2014 Artima, Inc. All Rights Reserved. - Privacy Policy - Terms of Use - Advertise with Us