On 2004 July 26 Monday 13:46, haskell@alias.spaceandtime.org wrote:

According to Enderton, one of the ways to define an ordered pair (a,b) is {{a},{a,b}}. A relation is defined as a set of ordered-pairs. A map, of course, is a single-valued relation.

The motivation for defining ordered pairs that way is more mathematical than type-theoretic. It arises from having sets as a starting point, and needing to define ordered pairs, relations, and functions.

Given all that, suppose I have a "FiniteMap Int String" in Haskell. This is, according to the definitions above, a "Set (Int,String)".

You have run into a problem expressing your meaning, because (Int, String) indicates a specific type in Haskell which is _not_ a Set.

An element of that has type (Int,String), which contains {Int,String}. But that can't exist because a Set contains only elements of one type.

The ordered pair 1,"one" would be represented as {{1},{1,"one"}}. Now, {1,"one"} can't exist in Haskell as you say, but it can be represented using the Either type constructor. Either enables a value to be chosen from two otherwise incompatible types. Either Int String is a type which can have values that are Ints or Strings, but the value must specify which using the Left or Right constructor. Left 5 and Right "five" are both values of the type Either Int String. Left "five" would be invalid. Instead of {1,"one"), in Haskell you would have {Left 1, Right "one"} of type Set (Either Int String). The ordered pair would be {Left {1}, Right {Left 1, Right "one"}} of type Set (Either Int (Either Int String)) and the finite map would be Set (Set (Either Int (Either Int String))) Few people would be able to tolerate writing a program using this type. :-)