Stories
Slash Boxes
Comments
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.
 Full
 Abbreviated
 Hidden
More | Login | Reply
Loading... please wait.
  • 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

    • > Naturals don't form a ring because they lack the
      > 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 :-) that don't have additive inverses.

      > 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.