Re: static types, checking, conversions
HaloO,
Larry Wall wrote:
On Wed, Apr 16, 2008 at 04:29:23PM +, [EMAIL PROTECTED] wrote:
: my Dog $spot = .new();
:
: to
:
: my $Spot = Dog.new();
:
: when you remove the declaration.
You'd also break multiple dispatch rather badly...
Sorry, why that? Isn't the dispatch on the dynamic type
of the value stored in $spot? Or are you talking about
dispatching .new itself?
sub foo (Dog $d) {...}
foo(.new); # .new called in Dog item context?
# with $d as invocant?
Regards, TSa.
--
The unavoidable price of reliability is simplicity
-- C.A.R. Hoare
Re: static types, checking, conversions
HaloO, Mark J. Reed wrote: Type checking in both js2/ecma4 and p6 is not merely documentation. It is enforced, but only if present. This is a tricky thing to achieve, which is why I suggested reading the js stuff to see how they went about it. I like the 'like' operator that does a structural inspection. Would that be worth an addition to Perl 6? We already have 'can' for single methods. Regards, TSa. -- The unavoidable price of reliability is simplicity -- C.A.R. Hoare
Re: static types, checking, conversions
HaloO,
[EMAIL PROTECTED] wrote:
You should look at Common Lisp. it's definition of optional typing
is that if you take a correct program and remove all the type
declarations, then it still works correctly, although it may be
significantly less efficient. Larry and i have discussed this and that
was his goai in Perl.
Wow, what is a correct program? I assume that there can be incorrect
type annotations then. I.e. if they introduce a type error that
wasn't there in the correct program before that it's the annotation's
fault, right?
Is this a correct implementation of Hello World?
sub foo ($x)
{
if $x == 13 { say Hello World! }
}
foo('13');
If yes, isn't it reasonable to annotate $x in foo with Int?
And would that produce a type error? IOW, is '13'.does(Int)
true? In nominal typing it should be false. But Str::ACCEPTS
could be a little smarter.
Now Perl doesn't quite meet that because of
inferred method dispatch on .new(). you need to change
Isn't it generally the case that assignment is
dispatched on the *static* type of the lhs? I surmise
that binding cannot be overloaded and this really is
where the type checker kicks in. But what exactly is
it supposed to do then?
I guess the generic answer is that there will be installable
pairs of dispatcher and binder. Which then raises the question
what the standard set will be :)
Regards, TSa.
--
The unavoidable price of reliability is simplicity
-- C.A.R. Hoare
Re: static types, checking, conversions
On Thu, Apr 17, 2008 at 09:24:47AM +0200, TSa wrote:
HaloO,
Larry Wall wrote:
On Wed, Apr 16, 2008 at 04:29:23PM +, [EMAIL PROTECTED] wrote:
: my Dog $spot = .new();
: : to
: : my $Spot = Dog.new();
: : when you remove the declaration.
You'd also break multiple dispatch rather badly...
Sorry, why that? Isn't the dispatch on the dynamic type
of the value stored in $spot?
Sure, but there are still meaningful declarations involved:
multi foo (Dog $d) {...}
multi foo (Hog $d) {...}
multi foo (Cat $d) {...}
multi foo (Rat $d) {...}
multi foo (Bat $d) {...}
If you remove those declarations the program breaks completely.
Larry
Re: static types, checking, conversions
HaloO, Mark J. Reed wrote: It would behoove @Larry to examine the optional type constraints system proposed for Javascript:TNG (see link from firefox.com developers page). I therefore assume that they have done so, but others would benefit by doing likewise. :) Do I get that right: you imply that I didn't do my homework? Note that I don't feel offended by that. I found two dissertations and a couple of papers about typing JavaScript. The quintessential is that optional typing is defined as having *no* impact on the dynamic behavior of the program. In that respect type annotations are like comments. I doubt that this is the case with Perl 6, or is it? Regards, TSa. -- The Angel of Geometry and the Devil of Algebra fight for the soul of any mathematical being. -- Attributed to Hermann Weyl
Re: static types, checking, conversions
Thom Boyer thom-at-boyers.org |Perl 6| wrote: Mark J. Reed wrote: It would behoove @Larry to examine the optional type constraints system proposed for Javascript:TNG (see link from firefox.com developers page). I therefore assume that they have done so, but others would benefit by doing likewise. :) Could you be a little more specific on where to find information on JavaScript's proposed system of type constraints? The firefox.com developers page (http://developer.mozilla.org/en/docs/Main_Page) has several links on JavaScript topics. The most promising one leads to http://developer.mozilla.org/en/docs/JavaScript, and, while that page has info on quite a few different versions of JavaScript, version 2 is not one of them. Of course, I'm only guessing that JavaScript 2 is what you might have meant by Javascript:TNG. (I can't find any mention of TNG or Next Generation on either of those pages, either.) =thom The links under ECMAscript 4, like Read the tutorial on evolutionary programming in ES4 http://www.ecmascript.org/es4/spec/evolutionary-programming-tutorial.pdf In http://www.ecmascript.org/. This paper shows how to add types to an untyped program as it grows. --John
Re: static types, checking, conversions
TSa Thomas.Sandlass-at-barco.com |Perl 6| wrote: I found two dissertations and a couple of papers about typing JavaScript. The quintessential is that optional typing is defined as having *no* impact on the dynamic behavior of the program. In that respect type annotations are like comments. I doubt that this is the case with Perl 6, or is it? Regards, TSa. In Perl 6, I'm trying to identify where type annotations affect behavior and when they don't. I think that's important since it separates the must-do analysis from optional optimization, and conversely describes what the optimizer can't do even if it thinks it could. As a degenerate case, not being allowed to assign or bind something is certainly an impact on behavior. If MMD is based on actual dynamic types, then static types don't affect the result, other than to prevent the program from loading the wrong thing into a variable that then gets used as a parameter. Also, look at: my Dog $spot .= new(Fido); the static type Dog does affect the subsequent use of .new. Even if you explain that in terms of the protoobject, the point is that saying Dog =does= something, it's not just a comment like a (current) Javascript naming convention. --John
Re: static types, checking, conversions
On Apr 16, 2008, at 3:44 , TSa wrote: I found two dissertations and a couple of papers about typing JavaScript. The quintessential is that optional typing is defined as having *no* impact on the dynamic behavior of the program. In that respect type annotations are like comments. I doubt that this is the case with Perl 6, or is it? My understanding is that Perl6 uses static typing as such (i.e. not merely comments) when it is provided. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] [EMAIL PROTECTED] system administrator [openafs,heimdal,too many hats] [EMAIL PROTECTED] electrical and computer engineering, carnegie mellon universityKF8NH
Re: static types, checking, conversions
Type checking in both js2/ecma4 and p6 is not merely documentation. It is enforced, but only if present. This is a tricky thing to achieve, which is why I suggested reading the js stuff to see how they went about it. On 4/16/08, Brandon S. Allbery KF8NH [EMAIL PROTECTED] wrote: On Apr 16, 2008, at 3:44 , TSa wrote: I found two dissertations and a couple of papers about typing JavaScript. The quintessential is that optional typing is defined as having *no* impact on the dynamic behavior of the program. In that respect type annotations are like comments. I doubt that this is the case with Perl 6, or is it? My understanding is that Perl6 uses static typing as such (i.e. not merely comments) when it is provided. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] [EMAIL PROTECTED] system administrator [openafs,heimdal,too many hats] [EMAIL PROTECTED] electrical and computer engineering, carnegie mellon universityKF8NH -- Sent from Gmail for mobile | mobile.google.com Mark J. Reed [EMAIL PROTECTED]
Re: static types, checking, conversions
You should look at Common Lisp. it's definition of optional typing is that if you take a correct program and remove all the type declarations, then it still works correctly, although it may be significantly less efficient. Larry and i have discussed this and that was his goai in Perl. Now Perl doesn't quite meet that because of inferred method dispatch on .new(). you need to change my Dog $spot = .new(); to my $Spot = Dog.new(); when you remove the declaration. -- Mark Biggar [EMAIL PROTECTED] [EMAIL PROTECTED] [EMAIL PROTECTED] -- Original message -- From: TSa [EMAIL PROTECTED] HaloO, Mark J. Reed wrote: It would behoove @Larry to examine the optional type constraints system proposed for Javascript:TNG (see link from firefox.com developers page). I therefore assume that they have done so, but others would benefit by doing likewise. :) Do I get that right: you imply that I didn't do my homework? Note that I don't feel offended by that. I found two dissertations and a couple of papers about typing JavaScript. The quintessential is that optional typing is defined as having *no* impact on the dynamic behavior of the program. In that respect type annotations are like comments. I doubt that this is the case with Perl 6, or is it? Regards, TSa. -- The Angel of Geometry and the Devil of Algebra fight for the soul of any mathematical being. -- Attributed to Hermann Weyl
Re: static types, checking, conversions
On Wed, Apr 16, 2008 at 04:29:23PM +, [EMAIL PROTECTED] wrote: : You should look at Common Lisp. it's definition of optional typing is that if you take a correct program and remove all the type declarations, then it still works correctly, although it may be significantly less efficient. Larry and i have discussed this and that was his goai in Perl. Now Perl doesn't quite meet that because of inferred method dispatch on .new(). you need to change : : my Dog $spot = .new(); : : to : : my $Spot = Dog.new(); : : when you remove the declaration. You'd also break multiple dispatch rather badly... Larry
Re: static types, checking, conversions
HaloO,
John M. Dlugosz wrote:
This needs to be fleshed out. Decisions need to be made.
Anyone want to discuss it with me?
I want to. But give me time. Meanwhile you could read
e.g. http://www.dcs.shef.ac.uk/~ajhs/classify/index.html.
This deals with F-bounded polymorphism in a tutorial
style. A generalisation of that is Constraint Bounded
Polymorphism as given in the papers of the WASP Group
at http://wasp.cs.washington.edu. Another inspiration
is the CDuce language http://www.cduce.org which is
built around semantic subtyping.
My point is that Perl 6 so far has defined a syntax
for type markup but hardly defined how typing works
---I remember the pain but no gain thread. It might
actually be the case that optional typing means that
you need a module that implements it.
I personally see types as the semantics of the code
with the added benefit of being machine readable and
thus can assist you in reasoning about the code.
A type system is a tool just like an IDE allows you
to browse the code, e.g. jumping to the definition of
a class or all invocations of a method etc.
There are two fundamental type errors in Perl 6:
1) a) no or b) ambiguous targets for dispatch
2) non-bindable args in non-dispatch position
1a and 2 can be easily avoided with slurpy Any
protos. So the only remaining offender is 1b. And
that might be pragmatized to just call them all.
So we sort of end up with the impossibility of
type errors :)
Your concerns so far have been with the typing of
assignment and binding. The former is easy because
it involves the creation of a new value. Thus one
can dispatch $x = $y on the container type of $x
and the value type of $y and store the result in
$x. So here you get an error of type 1 if any.
Binding is more complicated because there is no
new value involved but you want two containers
to share a value. This is where Larry's view concept
comes in to avoid the invariance problem of rw
containers. OTOH the synopsis say that binding
replaces the container, so
my Int $x = 13;
my Str $y = 'foo';
$y := $x;
$y = 42; # OK, type of $y now Int
but that contradicts the fact that binding happens
when functions are called
sub foo (Dog $d) { say $d; }
my Int $x = 23;
foo $x; # $d := $x makes type of $d Int and prints 23?
Note also that binding is specced only for scalars so far.
Not for elements of an array or hash!
Regards, TSa.
--
The Angel of Geometry and the Devil of Algebra fight for the soul
of any mathematical being. -- Attributed to Hermann Weyl
Re: static types, checking, conversions
It would behoove @Larry to examine the optional type constraints
system proposed for Javascript:TNG (see link from firefox.com
developers page). I therefore assume that they have done so, but
others would benefit by doing likewise. :)
On 4/15/08, TSa [EMAIL PROTECTED] wrote:
HaloO,
John M. Dlugosz wrote:
This needs to be fleshed out. Decisions need to be made.
Anyone want to discuss it with me?
I want to. But give me time. Meanwhile you could read
e.g. http://www.dcs.shef.ac.uk/~ajhs/classify/index.html.
This deals with F-bounded polymorphism in a tutorial
style. A generalisation of that is Constraint Bounded
Polymorphism as given in the papers of the WASP Group
at http://wasp.cs.washington.edu. Another inspiration
is the CDuce language http://www.cduce.org which is
built around semantic subtyping.
My point is that Perl 6 so far has defined a syntax
for type markup but hardly defined how typing works
---I remember the pain but no gain thread. It might
actually be the case that optional typing means that
you need a module that implements it.
I personally see types as the semantics of the code
with the added benefit of being machine readable and
thus can assist you in reasoning about the code.
A type system is a tool just like an IDE allows you
to browse the code, e.g. jumping to the definition of
a class or all invocations of a method etc.
There are two fundamental type errors in Perl 6:
1) a) no or b) ambiguous targets for dispatch
2) non-bindable args in non-dispatch position
1a and 2 can be easily avoided with slurpy Any
protos. So the only remaining offender is 1b. And
that might be pragmatized to just call them all.
So we sort of end up with the impossibility of
type errors :)
Your concerns so far have been with the typing of
assignment and binding. The former is easy because
it involves the creation of a new value. Thus one
can dispatch $x = $y on the container type of $x
and the value type of $y and store the result in
$x. So here you get an error of type 1 if any.
Binding is more complicated because there is no
new value involved but you want two containers
to share a value. This is where Larry's view concept
comes in to avoid the invariance problem of rw
containers. OTOH the synopsis say that binding
replaces the container, so
my Int $x = 13;
my Str $y = 'foo';
$y := $x;
$y = 42; # OK, type of $y now Int
but that contradicts the fact that binding happens
when functions are called
sub foo (Dog $d) { say $d; }
my Int $x = 23;
foo $x; # $d := $x makes type of $d Int and prints 23?
Note also that binding is specced only for scalars so far.
Not for elements of an array or hash!
Regards, TSa.
--
The Angel of Geometry and the Devil of Algebra fight for the soul
of any mathematical being. -- Attributed to Hermann Weyl
--
Sent from Gmail for mobile | mobile.google.com
Mark J. Reed [EMAIL PROTECTED]
Re: static types, checking, conversions
I apologize for the vagueness; I was away from browser when I sent that. Go to http://www.ecmascript.org for the nitty gritty on ECMAScript 4th Edition, a.k.a. JavaScript 2, which is what I was talking about. White papers, specs, reference interpreter. The link from the Firefox developers page (http://developer.mozilla.org/en/docs/Main_Page, which you get to by clicking the Developer tab on http://www.firefox.com) is called The Truth about Javascript, and leads to slides from Brendan Eich's talk at last year's Ajax Experience West conference (http://developer.mozilla.org/presentations/eich-ajax-experience-2007/). Embedded within the slides is discussion about what went into the design of Javascript 2, and a link over to the http://www.ecmascript.org site (as well as other interesting stuff).
Re: static types, checking, conversions
Mark J. Reed wrote: It would behoove @Larry to examine the optional type constraints system proposed for Javascript:TNG (see link from firefox.com developers page). I therefore assume that they have done so, but others would benefit by doing likewise. :) Could you be a little more specific on where to find information on JavaScript's proposed system of type constraints? The firefox.com developers page (http://developer.mozilla.org/en/docs/Main_Page) has several links on JavaScript topics. The most promising one leads to http://developer.mozilla.org/en/docs/JavaScript, and, while that page has info on quite a few different versions of JavaScript, version 2 is not one of them. Of course, I'm only guessing that JavaScript 2 is what you might have meant by Javascript:TNG. (I can't find any mention of TNG or Next Generation on either of those pages, either.) =thom
static types, checking, conversions
I posted my thoughts as a sort of white paper here: http://www.dlugosz.com/files/static-type.pdf This needs to be fleshed out. Decisions need to be made. Anyone want to discuss it with me? --John
