StrongRuby : gradual typing for Duby.

Abstract :

 

Static and dynamic type systems have well-known strengths and weaknesses. Statically typed programming languages incorporate a built-in static type system. Every legal program must successfully typecheck according to the rules of the type system.

 

Gradual typing provides the benefits of both static and dynamic checking in a single language by allowing the programmer to control whether a portion of the program is type checked at compile-time or run-time by adding or removing type annotations on variables. , that have no effect on the dynamic semantics of the language.

 

The complete proposal here : strongruby.pdf

Advertisements

3 comments so far

  1. Vidar Hokstad on

    It looks interesting, but I think it overlooks all that can be done through type inference alone, without annotations. Annotations are valuable for compilation to restrict the interface to separate compilation units, but a lot of inconsistencies can be caught by having the type checker annotate all functions with what types will cause certain classes of errors (any uncaught exception, for example)

  2. Pedro on

    hi Vidar.

    You are right, several cases can be cover by type inference, but the not all. For example the fibonacci.

    In the other hand, type inference for objects,IMO, is more complicated to developt. And I only and student applying to Google Summer of Code. The type inference is probably out of the scope of my knowledge.

  3. Vidar Hokstad on

    Actually, the type inference can be applied to anything – the limitation is on how much information you can infer (and that will affect how useful it is, of course). The key there is that the _type_ of an expression does not have to map to a class, but can equally well consist of a set of assertions that limits the possible values of the expression. That allows the inference to be much more specific.

    Without annotations a lot of the types inferred will be far more generic than they could be, that is true.

    The simplest approach to inference is just to walk the abstract syntax tree of a program from the leaves and up, marking each node as you go with the assertions you can make about the value of the expression, and at the same time adding any assertions you can make about the content of variables.

    For a typical recursive fibonacci implementation, the inferred types in Ruby will verge on being useless, as you’d probably only be able to restrict the inputs to any type that supports addition and subtraction operators.

    The key, though, is that if you have a type inference engine, you can treat any type annotation by just adding them to the set of assertions, and then check the set of assertions for consistency – the inference doesn’t need to be much more complicated than what you’d need to do to check the assertions in the first place.

    The combination means you need far fewer annotations – just by stating that the inputs are Fixnum for example, a relatively simple inference engine would be able to determine that the return type is also Fixnum. And if the function is used in any context where Fixnum is required, the engine could relatively easily determine whether the inputs also need to be Fixnum’s.

    Annotations can make it stricter, but are not required to check a lot of internal type consistency of the application as long as you have a set of defined error states. Note that I don’t believe it can be guaranteed to determine full consistency in Ruby without lots of restrictions – I’m pretty sure determining full consistency in Ruby is equivalent to the halting problem.

    If you’d like to discuss it further, feel free to e-mail me, and I’d be happy to explain more – I’d love to see someone actually do this with Ruby, but I doubt I’d have the time myself anytime soon.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: