Home » forums » LtU Forum

Logic operations on types

Hello everybody,

I ask you to excuse my ignorance in the question, I am a hobbyist programmer and I don't have any degree in CS. Recently I've found that some operations on types in advanced type systems are quite similar to logical operators.
For example, algebraic types are similar to exclusive OR operation, and multiple inheritance looks a lot loke AND operation.

I am sure this has been discovered and studied before (I can even remember reading about something similar in Wikipedia), but I cannot find any papers on the subject, probably because keywords like "type system" and "logical operators" do not really yield relevant results.

So, if such similarity exists, does it have a name? And what paper could you recommend that are relevant to this?

By catbert at 2009-09-05 22:44 | LtU Forum | previous forum topic | next forum topic | other blogs | 4646 reads

Comment viewing options

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

Calculus of Constructions

You might have more luck searching for "calculus of constructions", which is the logical framework that is normally used to formally describe type systems. As for discussion of how those abstractions fit into the semantics of any given programming language that seems to me like it would be more language specific and would be best served by a search specific to whatever languages you are interested in. If I were to make an educated guess I would say that ML would probably have the largest breadth of research into formalization and generalization of its type system.

By andrew johnson at Sun, 2009-09-06 00:31 | login or register to post comments

Curry-Howard

So, if such similarity exists, does it have a name?

The well-known Curry-Howard correspondence relates programs to logical proofs, and types to propositions. The latter correspondence relates logical operators in propositions to their type equivalents.

Previous Curry-Howard discussions on LtU include Relevance of Curry-Howard. Phil Wadler's paper/presentation Proofs are Programs is a good intro to the subject.

Automated proof assistants like Coq exploit Curry-Howard to be able to machine-check proofs. Coq depends on the Calculus of Inductive Constructions, which is an extension of the Calculus of Constructions mentioned by Andrew Johnson in another comment.

By Anton van Straaten at Sun, 2009-09-06 01:07 | login or register to post comments