[Grace-core] Should Grace abandon "gradual typing" for "like typing"?

[Erik Ernst]

Hello, 

I can add an extra fact on Dart here: It is possible for a class D to `implement` (not `extend`) a class C such that not all methods declared in C are actually implemented by D. This causes a warning at compile time and it causes `noSuchMethod` if any of these methods are invoked at runtime, but it does allow an instance of D to satisfy subtype checks for C. That is, a D is allowed to masquerade as a C, even in checked mode, as long as the missing methods are not actually invoked. This can be useful for various mock-up situations.

  best regards,

-- 
Erik Ernst   -   eernst at acm.org
Google, Inc.
________________________________________
Fra: Grace-core <grace-core-bounces at cecs.pdx.edu> på vegne af Vitek, Jan <j.vitek at northeastern.edu>
Sendt: 29. juli 2016 00:08
Til: James Noble
Cc: Tobias Wrigstad; grace-core at cecs.pdx.edu; Vitek, Jan; Laurence Tratt
Emne: Re: [Grace-core] Should Grace abandon "gradual typing" for "like typing"?

> if I've got a like type such as
>
> type Fooable = like { foo }     // something Fooable has a Foo method
>
> what happens if I assign an object that doesn't have a Foo method to that variable (and, say, never actually call the foo method).  Presumably that object is flowing in e.g. from a variable or parameter of type Unknown (aka Dynamic)
> so we don''t know at compile-time (or type-check type) whether or not
> the object is Fooable...
>
> method assignToFooable( other : Unknown  -> like Fooable  {
>      // now I'm being extra explicit other is dynamically typed
>      def x : like Fooable = other
>      return x
> }
>
> Does the assignment to a Fooable cause an error or not?  (I guess I should read the formalsims, but...)
>
> I thought Dart in checked mode *would* raise a dynamic error there.
> I thought Thorn would too, and if we can be sure that other does
> not have a foo method we get an eager error…?


No error in Thorn, Dart (unchecked), TypeScript, Hack.

But if you remove the “like” annotation, there will be an error.

-j

_______________________________________________
Grace-core mailing list
Grace-core at cecs.pdx.edu
https://mailhost.cecs.pdx.edu/mailman/listinfo/grace-core