This reminds me of categorial grammars. Has anyone here ever looked into them? I loved them. They're like simply typed lambda calculi but instead of a single arrow type there are two, one for the left and right side of a symbol. So you can so like:<p><pre><code> and : Phrase \ Conjunction / Phrase
do : Subject \ Verb / Object
</code></pre>
Sorry if I have the directionality wrong but `and` would take a phrase on the left, another on the right abd return a conjunction. `do` would take an Subject and an Object and return a verb. In STLC it would look like this:<p><pre><code> and : Phrase -> Phrase -> Conjunction
do : Subject -> Object -> Verb
</code></pre>
These are bad examples just for illustrations, consult real linguists.<p>Last time I looked at it they were adding polymorphism and a couple of people were starting to think about dependent types. It was mostly linguists interested in it but it was hardcore math and CS. Can't remember the names involved. Carl H. I forget what the H stands for. Hmm. Some fanous type theorists had written about them too.<p>Anyway, seemed relevant.