Home » forums » LtU Forum

Do we talk types over the phone?

I am pondering over some non-serious application of Curry-Howard isomorphism (CHI). Let's take any typical text in a natural language. What is its contents? Propositions or proofs? My judgement is that (almost?) exclusively propositions. Applying CHI, we can see that humans write mostly types. Already sounds strange.

Now, instead of a static text, let's analyze an interaction in a natural language (e.g., a conversation over a phone). People are still exchanging propositions, i.e., types. From this point I am trying to get back to computer science. Why isn't it so common that programs exchange types over the wire? Or rather, why cant we naturally see any programmatic interaction as an exchange of (exclusively) types? I suspect we can argue that transmitted values are just witnesses of the corresponding types, but still it is not natural, or at least traditional way to look at the issue. Why? Or did I make some mistake during my analysis of natural language part of the problem?

I know that "programmatic interaction" can be seen as a proof-reduction, but I am currently wearing more message-oriented hat.

By Andris Birkmanis at 2005-11-30 09:48 | LtU Forum | previous forum topic | next forum topic | other blogs | 6367 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Fashion?

I think it is just fashion. With a move away from exclusively statically typed languages, I predict that the pendulum will swing back to seeing types as values as quite normal - and thus exchanged.

By Alasdair Scott at Wed, 2005-11-30 10:06 | login or register to post comments

Not reflection or serialization

I agree that fashion has its influence.

I probably have to make a clarification - I do not mean possibility of exchanging some representations of types over the wire (a la Alice packages, and even they send a pair of value and its type, not just a type; and Java does not have anything except arrays of bytecode for this). I meant the way we look at communications, not the way we implement them.

By Andris Birkmanis at Wed, 2005-11-30 10:27 | login or register to post comments

Is there really a difference?

If types are only a form of classification, it doesn't seem to me to make much difference whether we are communicating the general or specific.

People are curious.

My government is shortsighted.

I have long thought that a study of philosophy is an essential pre-requisite for computer science.

By Alasdair Scott at Wed, 2005-11-30 11:08 | login or register to post comments

Categorial grammar

Applying CHI, we can see that humans write mostly types.

You can model natural language as propositions or as proofs, just as you can model computation using Prolog or Haskell.

Or did I make some mistake during my analysis of natural language part of the problem?

Yes. A type can be construed as a grammar, and a value of that type as a text matching that grammar. This is where the field of categorial grammar started. See:

Joachim Lambek. The mathematics of sentence structure, Amer. Math. Monthly 65. (1958) 154-170.

This seminal (and readable) paper used to be available on the web in HTML form but, alas, no longer it appears. In lieu of that, try Mark Jones' paper, Using Types to Parse Natural Language.

Update: I marked up the citation above with the link provided by bdonovan below.

By Frank Atanassow at Wed, 2005-11-30 16:20 | login or register to post comments

Lambek paper still available

This is just a note to say that the Lambek paper is still available online, though every link but one that I found via Google had rotted away. The sole working url seems to be:

http://wwwhomes.uni-bielefeld.de/gjaeger/lehre/cg_ss00/lambek/lambek58.html

Get it before it's gone. Better yet, if possible, mirror it online so that it doesn't disappear from the www.

By bdonovan at Thu, 2005-12-01 03:08 | login or register to post comments

Type theoretical grammar

Anyone interested in this area should look at Aarne Ranta's book "Type Theoretical Grammar" Indices 1, Oxford University Press, 1994.

By Neil Leslie at Fri, 2005-12-02 02:28 | login or register to post comments

Wow, a DSL

Thanks for the pointer!

I was pleased to find that the book is not the only source of information on the topic, and Type-Theoretical Grammar is very alive (fancy composing a letter in Russian with just a few mouse clicks? :-) ).

Please note that they have designed a DSL, which probably deserves a separate story.

By Andris Birkmanis at Fri, 2005-12-02 09:10 | login or register to post comments