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?
There's some work beyond just that. In particular work on how they
relate to induction, coinduction, and the mixing of the two; as well as
some type-theoretic issues having to do with the fact that you can
eta-expand records but not datatypes.
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: records are defined such that their projections give all the
information there is to be had. However, datatypes are defined by how
they can be constructed, and so that single constructor could bear some
intensional meaning that is not captured by the projections of its
fields. The constructors must have this intensional meaning, otherwise
we wouldn't be able to make sense of types with multiple constructors
bearing the same type of fields, e.g.:
data PreCantor a = Zero a | One a
-- Cantor = fix PreCantor
As an example of how single-constructor datatypes differ from records,
if we make the constructor(s) private then the datatype can be used to
implement witnesses; however, we cannot use records to implement
witnesses, because eta expansion means that everyone has free access to
the constructors of the record type.
--
Live well,
~wren
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
