On Thu, Feb 10, 2011 at 11:51 PM, wren ng thornton <[email protected]>wrote:
> On 2/11/11 1:16 AM, Sandro Magi wrote: > > On 2011-02-11 12:57 AM, wren ng thornton wrote: > >> This issue is an area of active research over in Agda. Their concerns > >> are (perhaps) quite a bit different since they're working with full > >> dependent types, but according to the type theory it definitely appears > >> that records (aka structs) are distinctly different from datatypes (aka > >> (recursive) tagged unions). To some extent they appear to be duals, > > > > I thought this was already well established, ie. records = products, > > datatypes = sums, and products and sums are duals. Or does the work > > you're referring to go beyond this simple characterization? > > Just saying that records = products and datatypes = sums doesn't explain > *why* records are different from datatypes with one constructor (i.e., > why is the sum of one product different from the product on its own). A > big part of this difference comes down to the eta-expandability of > records... Yes. Another way to say this is that the philosophy of clear-cut distinction between sum types and product types is a consequence of the fact that those classes have useful but distinct properties in category theory. In fact, BitC doesn't (at present) have anything that corresponds directly to a product type. The closest we have is structures. In ML/Haskell, records are merely a syntactic sugaring of tuples, which are a product type in the strictest sense. Because BitC structures place the binding of selectors in a context-dependent environment, it is not immediately obvious that they are merely syntactic sugar over tuples - and especially so since we don't actually *have* tuples! I'm reasonably confident that a desugaring analogous to the record desugaring exists, and that there is no deep theoretic problem here. That said, it is distinctly odd that the explanation of the semantics of structures in BitC relies on an appeal to a type that is required (because of this reduction) to be part of the core BitC type system and yet isn't expressable in the surface syntax. Tuples are coming back, so I think the problem is very temporary, but the current state is a head-scratcher to consider for any of you who are inclined to such things. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
