NOTE: use Perl; is on undef hiatus. You can read content, but you can't post it. More info will be forthcoming forthcomingly.
All the Perl that's Practical to Extract and Report
The Fine Print: The following comments are owned by whoever posted them. We are not responsible for them in any way.
an endless discussion thread about what features to include.
-- Jarkko Hietaniemi
Stories, comments, journals, and other submissions on use Perl; are Copyright 1998-2006, their respective owners.
I don't grok the syntax (Score:2)
OK, I'm at a loss here. Naturals don't form a ring because they lack the number zero? Is that right? If so, that seems straightforward enough. However, I don't know what you mean when you wrote that even though Naturals are rings, you seem to have proven they are. I certainly don't know what that means in relation to the code you posted.
Taking a guess, it seems what you're saying is that for a given set S which satisfies condition C, no arbitrary subset of S is necessarily guaranteed to satisfy C but
Re:I don't grok the syntax (Score:1)
> number zero?
This is somewhat beside the point, but that is one reason, yes. The other reason is that there are elements (namely, all of them
> Taking a guess, it seems what you're saying is
> that for a given set S which satisfies condition
> C, no arbitrary subset of S is necessarily
> guaranteed to satisfy C but you've accidentally
> implied that in your theory.
Precisely. It turns out that that's how I (tried to) define roles. The thing that makes a theory a role is that any subset of a set that satisfies a role also satisfies that role.
I'll explain the syntax a bit, even though in my new formulation it will mean something different.
^T represents any set: it is an unconstrained variable. Foo{^T} is a *predicate* on that set. And <= is a poor name for "given" or something (it's supposed to look like a backward "implies"). Basically, the expression ^T <= Foo{^T} can represent any set whose Foo constraint is satisfied.
The place where the error came in:
Ring{^T} < Num{^T}
Means "the Ring constraint is satisfied on a set ^T when the Num constraint is", or, interpreting the language a bit, "a set is a ring if all of its elements are numbers", which is clearly wrong.
As far as the new formulation, I am somewhat satisfied (though disappointed, as I no longer have a masters thesis) that it reduces to a minimal generalization of F<: polymorphic typing. That is, there is already a well-established body of literature on the subject, which means that Perl 6 is more likely to get it right.
Reply to This
Parent