Desc: definition of SUMD is broken

[GoogleCodeExporter]

Consider the (bootstrapped) definitions of SUMD:
> (PAIR (SIGMAD enumU (L $ HF "E" $ \_E ->
>     (SIGMAD (branchesDOp @@ [_E]) 
>         (L $ K (CONSTD UNIT)))))

and SIGMAD:
> (PAIR (SIGMAD SET (L $ HF "S" $ \_S -> 
>     (PRODD (PID _S (L $ K IDD)) 
>         (CONSTD UNIT))))

SIGMAD takes a set S and a function from S to descriptions, itself given by
a description (using PID and IDD). However, SUMD takes an enumeration E and
a set of branches, and branchesDOp returns a tuple of the *set* desc
(rather than using IDD). I am not sure this is well-founded, and it means
box gives the wrong answer when applied to SUMD (see ./test/BugBoxSum.pig).

I can't see an obvious way to fix this while keeping SUMD meaningfully
distinct from SIGMAD. Perhaps we could use PRODD in the definition of SUMD
as PID is used in the definition of SIGMAD?

Original issue reported on code.google.com by adamgundry on 13 May 2010 at 10:44

[GoogleCodeExporter]

As I see it, we have two choices (neither of which I have investigated 
thoroughly).
We can retreat, using a function to store the branches in SUMD, so that SUMD 
becomes
exactly the enumeration special case of SIGMAD. Or we can attack, and figure 
out how
to give some coded treatment of finite products, either by computing an iterated
binary product by recursion over _E, or by adding a code for products whose 
domain is
an enumeration.

What do we lose if we retreat?

Original comment by co...@strictlypositive.org on 14 May 2010 at 9:01

[GoogleCodeExporter]

In terms of what is actually implemented so far, very little use is made of the
SUMD/SIGMAD distinction, so we wouldn't lose much. In fact, some code would 
probably
become a bit simpler. I was wondering about abolishing SUMD altogether, but I 
guess
it would still be useful for writing some generic programs as you would have 
access
to the enumeration.

My inclination is to retreat; one can always reconstruct the branches from the
function should they be necessary.

Original comment by adamgundry on 14 May 2010 at 9:54

[GoogleCodeExporter]

By the way, is this Desc we're talking about? If so, retreat is far more 
attractive.

I worry that we are investing too much effort in the Desc universe, when IDesc 
is the
real deal. Of course, similar issues will arise.

But we should focus on getting IDesc right and using it.

Original comment by co...@strictlypositive.org on 14 May 2010 at 10:22

[GoogleCodeExporter]

Yes, this is for Desc, though we will have a similar issue for IDesc if we want 
to
levitate it with finite sums. As far as I am aware, nobody has looked at 
levitating
IDesc yet, and it is rather less developed. Is levitation a reasonable next 
step?

Original comment by adamgundry on 14 May 2010 at 11:11

[GoogleCodeExporter]

Overdue, methinks. Sounds like a candidate for next week's fun and games (with 
JC and
PM in town). It'd be good to port Desc technology over.

Original comment by co...@strictlypositive.org on 14 May 2010 at 11:21

[GoogleCodeExporter]

I have retreated and switched SUMD over to using a function. My assertion that 
we
wouldn't lose much was not quite accurate; equation solving becomes harder 
thanks to
the higher-order representation, so some of the argument synthesis stopped 
working. I
think we can get it back without too much trouble though.

I will open a new issue for levitating IDesc.

Original comment by adamgundry on 17 May 2010 at 7:46

• Changed state: Fixed