[Haskell-cafe] Type Theory? Relations

2004-07-26 Thread haskell
Hello,

I have a question that may pertain to type theory.

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.

Given all that, suppose I have a FiniteMap Int String in Haskell. 
This is, according to the definitions above, a Set (Int,String).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.

What I'm getting at is that it seems that a Relation should be defined

type Relation a = Set (a,a)

rather than 

type Relation a b = Set (a,b)

so that we don't have this problem.

Thanks.
___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] Type Theory? Relations

2004-07-26 Thread Scott Turner
On 2004 July 26 Monday 13:46, [EMAIL PROTECTED] 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. :-)
___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe