Re: [Haskell-cafe] The semantics of constructor patterns

2007-12-30 Thread Jonathan Cast 

On 30 Dec 2007, at 11:10 AM, Cristian Baboi wrote:

In section 4.3.3., chapter 4: Structured types and the semantics of  
pattern-matching,  by S.Peyton Jones and Philip Wadler, there is  
this equation:


Eval[[\(s p1 p2 ... pt).E]] (s a1 a2 ...at) = Eval[[\p1 ... \pt.E]]  
a1 ... at


The text say:
To apply \(s p1 ... pt).E to an argument A we first evaluate A to  
find out what sort of object it is.
Finally, if A was built with the same constructor as the patern,  
then the first rule applies.


What I don't get it :

(s a1 a2 ... at) must be the value of A in the semantic domain. Let  
call that value a.
Then how can one know if a was built with (s a1 a2 ... at) and not  
with (egg b1 b2) ?


I suspect that s and egg are constructors, in which case their images  
are (by definition) mutually exclusive.


jcc

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] The semantics of constructor patterns

2007-12-30 Thread Cristian Baboi 
On Sun, 30 Dec 2007 19:13:47 +0200, Jonathan Cast  
[EMAIL PROTECTED] wrote:



On 30 Dec 2007, at 11:10 AM, Cristian Baboi wrote:

In section 4.3.3., chapter 4: Structured types and the semantics of  
pattern-matching,  by S.Peyton Jones and Philip Wadler, there is this  
equation:


Eval[[\(s p1 p2 ... pt).E]] (s a1 a2 ...at) = Eval[[\p1 ... \pt.E]] a1  
... at


The text say:
To apply \(s p1 ... pt).E to an argument A we first evaluate A to find  
out what sort of object it is.
Finally, if A was built with the same constructor as the patern, then  
the first rule applies.


What I don't get it :

(s a1 a2 ... at) must be the value of A in the semantic domain. Let  
call that value a.
Then how can one know if a was built with (s a1 a2 ... at) and not with  
(egg b1 b2) ?


I suspect that s and egg are constructors, in which case their images  
are (by definition) mutually exclusive.


I have not seen that definition in the book.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] The semantics of constructor patterns

2007-12-30 Thread Benja Fallenstein 
Hi Cristian,

On Dec 30, 2007 6:10 PM, Cristian Baboi [EMAIL PROTECTED] wrote:
 What I don't get it :

 (s a1 a2 ... at) must be the value of A in the semantic domain. Let call
 that value a.
 Then how can one know if a was built with (s a1 a2 ... at) and not with
 (egg b1 b2) ?

Because the semantic domain is chosen so that (s a1 a2 ... at) and
(egg b1 b2) are distinct objects.

More precisely, the domain corresponding to (for example) the type

data T = C1 T11 T12 | C2 T21 T22

should be isomorphic to the domain

[[T]] = lift (([[T11]] * [[T12]]) + ([[T21]] * [[T22]]))

where * is cartesian product, + is disjoint sum (e.g., X+Y = {(1,x) |
x in X} union {(2,y) | y in Y}, and 'lift' adds the bottom element to
the domain.

So here, C1 and C2 correspond to the two sides of the disjoint sum,
meaning you can tell them apart.

Hope that helps?

- Benja
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] The semantics of constructor patterns

2007-12-30 Thread Cristian Baboi 
Thank you. The thing is that when talking about the semantic of Prolog,  
one can choose any set as the semantic domain to start, and then a reason  
is given for choosing the Herbrand universe.


On Sun, 30 Dec 2007 19:23:00 +0200, Benja Fallenstein  
[EMAIL PROTECTED] wrote:



Hi Cristian,

On Dec 30, 2007 6:10 PM, Cristian Baboi [EMAIL PROTECTED] wrote:

What I don't get it :

(s a1 a2 ... at) must be the value of A in the semantic domain. Let call
that value a.
Then how can one know if a was built with (s a1 a2 ... at) and not with
(egg b1 b2) ?


Because the semantic domain is chosen so that (s a1 a2 ... at) and
(egg b1 b2) are distinct objects.

More precisely, the domain corresponding to (for example) the type

data T = C1 T11 T12 | C2 T21 T22

should be isomorphic to the domain

[[T]] = lift (([[T11]] * [[T12]]) + ([[T21]] * [[T22]]))

where * is cartesian product, + is disjoint sum (e.g., X+Y = {(1,x) |
x in X} union {(2,y) | y in Y}, and 'lift' adds the bottom element to
the domain.

So here, C1 and C2 correspond to the two sides of the disjoint sum,
meaning you can tell them apart.

Hope that helps?

- Benja



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe