21–30 of 43 posts
Then we interface with the AST of any language and we can stop re-iventing the wheel every two week...
It is so crazy ?
Nobody tried it before ?
Really cool idea! I like that you can specify a `#respond_to?` constraint instead of a class. Not sure if OP is the author, but here's some feedback: * It would be better if this didn't pollute the global namespace by defining `#typesig` in `Module` [0] -- perhaps consider refactoring that method into a module which the user may extend. Doing so would also get you out of needing to define `Module#prepend` for older v…
typesig :sum, [:to_i, Numeric] => Numeric
also, the global switch is simple:
if $DEBUG
require 'rubype'
else
def typesig(*args) end
end
http://www.cs.umd.edu/projects/PL/druby/
Some features:
--------------
Type inference:
DRuby uses inference to model most of Ruby’s idioms as precisely as possible without any need for programmer intervention.
Type annotations:
Methods may be given explicit type annotations with an easy to use syntax inspired by RDoc.
Dynamic checking:
When necessary, methods can be type checked at runtime, using contracts to isolate and properly blame any errant code, similar to gradual typing.
Metaprogramming support:
DRuby includes a combined static and dynamic analysis to precisely model dynamic meta-programming constructs, such as eval and method_missing.
Earlier quoted context omitted.
This is kind of pedantic. What programmers think of and find useful as types and type systems is quite different from what type theorists think.
I would definitely find what curryhoward described as useful, but I don't think Ruby is that language in which it should) be implemented. That being said, sum types would be a nice addition to this library.
> When most practitioners think of "typechecking", they typically think about proving properties about programs statically.
This is what the type theory community (e.g. Bob Harper) thinks...not anyone else from what I can tell (definitely not practicing programmers).
Typing it out on mobile didn't make it easy to do the right quote context. Here is a good essay about it all:
http://www.cl.cam.ac.uk/~srk31/research/papers/kell14in-auth...
vs. say
https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...
There are other ways to do typing that might make more sense for a dynamic language than going down the expressiveness rabbit hole; e.g.
Earlier quoted context omitted.
I would definitely find what curryhoward described as useful, but I don't think Ruby is that language in which it should) be implemented. That being said, sum types would be a nice addition to this library.
I was only referring to the starting quote: > When most practitioners think of "typechecking", they typically think about proving properties about programs statically. This is what the type theory community (e.g. Bob Harper) thinks...not anyone else from what I can tell (definitely not practicing programmers). Typing it out on mobile didn't make it easy to do the right quote context. Here is a good essay about it all…
I'm not saying that types or typechecking are inherently static concepts. I'm also not saying that this library should do static typechecking—that would be an absurd demand. I only meant that the wording is misleading.
Even more misleading is author's use of the term "gradual type checking", which has a well-understood meaning: the ability to add static checks to an otherwise dynamically-typed program.
When most practitioners think of "typechecking", they typically think about proving properties about programs statically. This project seems equivalent to adding a runtime check at each call site to ensure the arguments and return values are the correct type. This is certainly useful sometimes, as it gives programs the desirable "fail fast" property. But it isn't "typechecking" as most engineers understand it. Or at…
This is kind of pedantic. What programmers think of and find useful as types and type systems is quite different from what type theorists think.
Earlier quoted context omitted.
I was only referring to the starting quote: > When most practitioners think of "typechecking", they typically think about proving properties about programs statically. This is what the type theory community (e.g. Bob Harper) thinks...not anyone else from what I can tell (definitely not practicing programmers). Typing it out on mobile didn't make it easy to do the right quote context. Here is a good essay about it all…
Perhaps it's true that many programmers don't realize the fundamental connection between typechecking and theorem proving (i.e., that they are the same thing). But that wasn't meant to be the point. The point is that when most programmers hear the word "typechecking", they think of compile-time typechecking. This word is usually used in a static context. I'm not saying that types or typechecking are inherently static…
Most programmers don't think "dynamic type checking" is a misnomer, while it is true that "type checking" itself leans towards a static connotation.
I've seen gradual type checking used both ways in the literature, actually. Wiki has the term defined for dual phase:
http://en.wikipedia.org/wiki/Gradual_typing
> Gradual typing is a type system in which variables may be typed either at compile-time (which is static typing) or at run-time (which is dynamic typing), allowing software developers to choose either type paradigm as appropriate, from within a single language.
I'm sure this is just poor writing (as Siek defines it, it should be from dynamic to static), but there is enough confusion here where you might bother using the term for adding stronger dynamic type checks to an otherwise less dynamically typed language (if you admit dynamic types as types, of course). Also, a dynamically checked type signature is the first step to a statically typed one (as long as your types remain weak enough that static typing is achievable in the future). So in that sense, it is "gradual" typing, just from a meta perspective :)
> This gem brings you advantage of type without changing existing code's behavior. I'm fairly sure it changes the performance characteristics of code it is applied on. I'd recommend adding benchmarks to the README so prospective users might be aware of this beforehand.
Ruby is flexible enough to allow quite a bit of experimentation with stuff like that. Especially because classes can be re-opened, so if worried about performance, it'd be easy enough to allow type annotations (or whatever other extensions people come up with) to live in separate files if people want them to, and conditionally include them only as needed/wanted.
When most practitioners think of "typechecking", they typically think about proving properties about programs statically. This project seems equivalent to adding a runtime check at each call site to ensure the arguments and return values are the correct type. This is certainly useful sometimes, as it gives programs the desirable "fail fast" property. But it isn't "typechecking" as most engineers understand it. Or at…
One thing we've applied on a Python(2, unfortunately, so can't go deep on the static type analysis) is enable this sort of type hinting when running our app in debug or test mode. Obviously can't catch everything, but it catches some of the sillier bugs.
I find that putting the method signature at the end of the method definition can become unreadable pretty fast. Also, the fact that it doesn't offer any performance improvement (most probably, this will actually degrade performance) makes me see this as a cool trick, but not really recommended in production. I like the aproach Perl 6 took on gradual typing. You can read about it in this article which computes fibonna…
typesig def meth(arg) arg end, [Numeric] => Numeric
Although it's still end of the method, it already suggests that signature will be there