Hi.
Claus Reinke writes:
> - one would think that () simply takes its role as a unit, so that
> (),a == a == a,()
> but if we know x::() does that imply that x,a == a ?
> x could be bottom, and the equations for the unit look strict in their
> unit parameter, so probably not;
<possible gross ignorance>
Does that matter, if the () can't be retrieved from the product by
pattern matching? Could Void be (reinstated and) used as the unit for
products?
</possible>
> [...]
>
> So I would like to know: are there any programming languages
> with associative products, and is there any real point against
> this feature (beyond "unusual")?
>
> In case you don't just like the puzzle for the puzzle's sake, there
> are two practical motivations for this:
>
> - the current "products" in Haskell are a pain
> - extensible records in TREX use associative commutative
> construction and matching, but built-in for one specific
> construct (rows); it would be nice if these properties of
> constructors could be supported more generally, and
> extensible records be built on top of such general support
This is relevant to my (continuing) attempts to type a natural join.
Starting with TREX row types like this:
(foo::a, bar::b | r)
-- Rows with a type a field labelled foo, a type b field labelled
-- bar, and possibly some other fields
I'd like to add row type constructors (||), (-), and (&&):
(r || s)
-- The catenation of r with s, which would always be predicated by
-- r and s having no common labels
(r - s)
-- The row type with the fields of r whose labels are not in s
(r && s)
-- The row type with the fields of r whose labels are also in s,
-- which would always be predicated by r and s having unifiable
-- types for those fields
so that a natural join (of records) could have this type:
Eq (Rec (r && s)) => Rec r -> Rec s -> Maybe (Rec (r || (s - r)))
with extensions to the predicate because of the use of (&&).
An issue arises in unifying two types like (r || s) and (foo::a). It
isn't apparent whether to substitute (foo::a)/r and EmptyRow/s, or
vice versa. With modular compilation, the information simply isn't
there, so some further rule would need to be imposed.
------
>From even longer ago in the thread...
Matt's :, constructor is similar to the idea of using a class to help
implement tuples. I forget where I saw it (maybe a passing mention in
http://www.dcs.glasgow.ac.uk/jfp/bibliography/jfp92.html#Jones1992:475)
but IIRC the gist is:
class Tuple a
data T a b = T a b
instance Tuple ()
instance Tuple b => Tuple (T a b)
which would all be hidden from the programmer, and generated when
desugaring (,) and (,,) and so on.
Regards,
Tom
