Ambidexter tutorial
lesson 1
and types, function types, True

introduction

This is a lesson in Logic and Programming. Both of these fields of study originated in the first part of the 20th century, but the close relationship between proofs and programs was not well known or understood. The understanding has arrived in the last 10 to 20 years. However, most people familiar with both programming languages and logic are still unaware of the connection.

There is a deep relationship between the two which Curry, Howard, and de Bruijn elucidated.

(In about 1969 I took a course in formal logic from the philosophy department at Harvard. It taught a system of logic called Natural Deduction, developed by Gentzen in the 1930's. I had already done some computer programming, but was away from it until 1973 and I really got back to it in 1976. At that time Pascal was an up and coming language, and it was a big deal when the inventor of Pascal came up with a new language with modules to support abstraction, Modula. In the early 80's Ada was developed with modules and generics. A few years later, at about the time when object-oriented languages were becoming popular due to their support for abstraction, in 1988 a paper titled Abstract types have existential type appeared in a journal that I was receiving which made Natural Deduction into a programming language. It did so in a straightforward way. It had abstraction and generics, and achieved this effortlessly and without imposing limitations on the way its constructs could be combined. I was astonished. People (myself included) had been spending much effort toward these goals of programming language design when an excellent framework for solution had been staring them in the face all this time.)

examples

• true.ambi
• false.ambi
• and1.ambi
• and2.ambi
• implication1.ambi

exercise

• Write a program which uses a type different from any of those in the example programs.