6 ms·

From the static typing POV, the dualism is imaginary because gradual types are a perfectly acceptable and long known static type system. This is the real point

by tel 12y ago

From the static typing POV, the dualism is imaginary because gradual types are a perfectly acceptable and long known static type system. This is the real point of the "unityped" argument.

raiph 12y ago
Right. I think it's reasonable to say that all P6 code is statically typed, using nominal typing.[1] I've not actually checked the following code yet. I just wanted to post it now and will return to update after I've tested this stuff tonight, but here's what I'm currently thinking: * The Any type is the default value type. * Built-in literals are automatically converted in to more specific value types at the time they are encountered by the compiler: my $a; # $a contains an `(Any)` aka an undefined Any $a = 42; # puts an Int value into $a * User defined literals and run-time string input are also supposed to be optionally automatically converted from an Any into a more specific type on assignment, but that's not yet implemented in the Rakudo P6 compiler. * Optional explicit types improve type-checking on assignment: my Int $d = 22/7; # compile-time error * Not yet implemented but due to land soon: my Int(Any) $e = 22/7; # coerces 22/7 (a Rat, thus an Any) # to 3 (an Int) at compile-time * And for calls: sub add (Int $x, Int $y) { $x + $y } my $a = 42; my $b = '42'; my Str $c = '42'; add($a, $a); # OK add($a, $b); # run-time error? add($a, $c); # compile-time error * Optional explicit types enable multisub dispatch: sub add (Int $x, Str $y) { say "oops!" } add($a, $c); # resolves to above sub at compile-time # says "oops!" at run-time * P6 allows users to introduce "subsets". Subsets combine a base type (always static/compile-time) with additional constraint logic. The additional constraint may force the subset to become partially dynamic rather than solely static. * Subsets can be applied in an assignment or signature: my enum Day ['Sun','Mon','Tue','Wed','Thu','Fri','Sat']; subset Weekday of Day where 'Mon' .. 'Fri'; my Weekday $wd = Sat; # compile-time error sub foo (Weekday $wd) { ... } * The additional constraint logic of a subset is a P6 "smart match" -- arbitrary code that accepts or rejects a specific value of the base type. In the Weekday subset above the constraint logic is `'Mon' .. 'Fri';`. * If code analysis can deduce a finite set from the combination of base type and the additional constraint logic, then a compiler may choose to make the whole subset static and check and resolve calls and constrained assignments at compile-time. Otherwise the static part of a subset is checked at compile-time, which may lead to a particular call being among the candidates for a final dispatch, and then there may be a final round of call resolution and checking at run-time. * Assignments and function calls that don't involve dynamic subsets, or where the compiler can eliminate them from consideration at compile-time, are type checked and dispatch resolved at compile-time. * Methods are always dispatch resolved at run-time. [1] http://en.wikipedia.org/wiki/Nominal_type_system http://en.wikipedia.org/wiki/Nominal_type_system
- tel 12y ago
  The idea of trying to move subset types forward is interesting. Using an SMT solver [0] you can move quite a bit forward. Otherwise, generally, you're talking about associating a dictionary of pre- and post-conditions with a type (e.g., Weekday is a new nominal type isomorphic with Day, but it also has an associated dict containing checks that it's within Mon-Fri). Carrying that dict around has been well-solved by Haskell's typeclass compilation machinery and then it's just a matter of inserting the checks at the right times and not more often, I suppose. [0] http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/ http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/
  - raiph 12y ago
    Perhaps you're aware that one of the biggest influences on P6 was Haskell and the 2005-2007 Audrey Tang / Pugs / lambdacamels era. Loads of crazy smart kids sharing wild thoughts with Larry, Damian etc. and writing the first P6 compiler in Haskell.
    - tel 12y ago
      I'm dimly aware, but that was prior to my time. I'm definitely able to see the influences, though! :)
cbd1984 12y ago
> the "unityped" argument. Which is a gross, deliberate misunderstanding of how dynamic typing works.
- tel 12y ago
  I'm sure that's not the case; instead, normally, it's an intentional distinction between the kind of things that "static types" are and the kind of things that "dynamic types" are. Merely because they share an informal descriptor doesn't make them comparable. The unityped argument states only that any language admits a static type analysis regardless of whether it admits to it in polite company. From here gradual types are natural: just embed the unitype into a richer static type system. If there's a dynamic type system (called a "tag" system sometimes to ensure distinctiveness) then that all lives after these types have run. It can be influenced by these types, but it is certainly more than merely syntactic/logical which gives it different correctness/behavior/UX properties.
  - cbd1984 12y ago
    No. Dynamic types are not tags. They're types, regardless of what static type zealots insist.
    - tel 12y ago
      I'm not sure what you're arguing. If you're trying to equate "dynamic types" with "(static) types" then I'd like to see how you're doing that. If you're trying to refute that "dynamic types" are "tags" then I'd like to hear your definition of "tags" which you feel inappropriately characterizes "dynamic types". If you're arguing something like "both 'static types' and 'dynamic types' are elements of a larger class of things called 'types'" then I'd be happy to talk about that given a meaningful definition of this larger class "types". Generally, however, I find that most definitions of this larger class of "types" are difficult to operationalize. Due to that, please re-read my responses and mentally impute "static types" wherever I say "types". I try to be explicit about this, and it is my general MO, so if any disagreement or misunderstanding still remains then I'd be happy to talk about that as well.

by tel 12y ago

From the static typing POV, the dualism is imaginary because gradual types are a perfectly acceptable and long known static type system. This is the real point of the "unityped" argument.

raiph 12y ago

Right. I think it's reasonable to say that all P6 code is statically typed, using nominal typing.[1] I've not actually checked the following code yet. I just wanted to post it now and will return to update after I've tested this stuff tonight, but here's what I'm currently thinking: * The Any type is the default value type. * Built-in literals are automatically converted in to more specific value types at the time they are encountered by the compiler: my $a; # $a contains an `(Any)` aka an undefined Any $a = 42; # puts an Int value into $a * User defined literals and run-time string input are also supposed to be optionally automatically converted from an Any into a more specific type on assignment, but that's not yet implemented in the Rakudo P6 compiler. * Optional explicit types improve type-checking on assignment: my Int $d = 22/7; # compile-time error * Not yet implemented but due to land soon: my Int(Any) $e = 22/7; # coerces 22/7 (a Rat, thus an Any) # to 3 (an Int) at compile-time * And for calls: sub add (Int $x, Int $y) { $x + $y } my $a = 42; my $b = '42'; my Str $c = '42'; add($a, $a); # OK add($a, $b); # run-time error? add($a, $c); # compile-time error * Optional explicit types enable multisub dispatch: sub add (Int $x, Str $y) { say "oops!" } add($a, $c); # resolves to above sub at compile-time # says "oops!" at run-time * P6 allows users to introduce "subsets". Subsets combine a base type (always static/compile-time) with additional constraint logic. The additional constraint may force the subset to become partially dynamic rather than solely static. * Subsets can be applied in an assignment or signature: my enum Day ['Sun','Mon','Tue','Wed','Thu','Fri','Sat']; subset Weekday of Day where 'Mon' .. 'Fri'; my Weekday $wd = Sat; # compile-time error sub foo (Weekday $wd) { ... } * The additional constraint logic of a subset is a P6 "smart match" -- arbitrary code that accepts or rejects a specific value of the base type. In the Weekday subset above the constraint logic is `'Mon' .. 'Fri';`. * If code analysis can deduce a finite set from the combination of base type and the additional constraint logic, then a compiler may choose to make the whole subset static and check and resolve calls and constrained assignments at compile-time. Otherwise the static part of a subset is checked at compile-time, which may lead to a particular call being among the candidates for a final dispatch, and then there may be a final round of call resolution and checking at run-time. * Assignments and function calls that don't involve dynamic subsets, or where the compiler can eliminate them from consideration at compile-time, are type checked and dispatch resolved at compile-time. * Methods are always dispatch resolved at run-time. [1] http://en.wikipedia.org/wiki/Nominal_type_system http://en.wikipedia.org/wiki/Nominal_type_system

tel 12y ago
The idea of trying to move subset types forward is interesting. Using an SMT solver [0] you can move quite a bit forward. Otherwise, generally, you're talking about associating a dictionary of pre- and post-conditions with a type (e.g., Weekday is a new nominal type isomorphic with Day, but it also has an associated dict containing checks that it's within Mon-Fri). Carrying that dict around has been well-solved by Haskell's typeclass compilation machinery and then it's just a matter of inserting the checks at the right times and not more often, I suppose. [0] http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/ http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/
- raiph 12y ago
  Perhaps you're aware that one of the biggest influences on P6 was Haskell and the 2005-2007 Audrey Tang / Pugs / lambdacamels era. Loads of crazy smart kids sharing wild thoughts with Larry, Damian etc. and writing the first P6 compiler in Haskell.
  - tel 12y ago
    I'm dimly aware, but that was prior to my time. I'm definitely able to see the influences, though! :)

cbd1984 12y ago

> the "unityped" argument. Which is a gross, deliberate misunderstanding of how dynamic typing works.

tel 12y ago
I'm sure that's not the case; instead, normally, it's an intentional distinction between the kind of things that "static types" are and the kind of things that "dynamic types" are. Merely because they share an informal descriptor doesn't make them comparable. The unityped argument states only that any language admits a static type analysis regardless of whether it admits to it in polite company. From here gradual types are natural: just embed the unitype into a richer static type system. If there's a dynamic type system (called a "tag" system sometimes to ensure distinctiveness) then that all lives after these types have run. It can be influenced by these types, but it is certainly more than merely syntactic/logical which gives it different correctness/behavior/UX properties.
- cbd1984 12y ago
  No. Dynamic types are not tags. They're types, regardless of what static type zealots insist.
  - tel 12y ago
    I'm not sure what you're arguing. If you're trying to equate "dynamic types" with "(static) types" then I'd like to see how you're doing that. If you're trying to refute that "dynamic types" are "tags" then I'd like to hear your definition of "tags" which you feel inappropriately characterizes "dynamic types". If you're arguing something like "both 'static types' and 'dynamic types' are elements of a larger class of things called 'types'" then I'd be happy to talk about that given a meaningful definition of this larger class "types". Generally, however, I find that most definitions of this larger class of "types" are difficult to operationalize. Due to that, please re-read my responses and mentally impute "static types" wherever I say "types". I try to be explicit about this, and it is my general MO, so if any disagreement or misunderstanding still remains then I'd be happy to talk about that as well.