[Haskell-cafe] The semantics of constructor patterns

[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  
<benja.fallenstein at gmail.com> wrote:

> Hi Cristian,
>
> On Dec 30, 2007 6:10 PM, Cristian Baboi <cristian.baboi at gmail.com> 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