Hi Chris, Many of your ideas are already implemented in Typed Racket.
For using the context of following the current branch to refine the type, see occurrence typing (paper, "Logical Types For Untyped Languages"). Typed Racket combines static checks and runtime contracts in a very cool way. You can statically type check *untyped* code by declaring types for the interfaces to untyped land. Typed land will treat it statically, and the untyped boundary will be checked at runtime. I'm currently in progress with Typed Clojure, which boils down to taking everything relevant from Typed Racket and adapting it to Clojure, plus some extra stuff for "ad-hoc object" maps, multimethods, protocols, JVM integration etc. https://github.com/frenchy64/typed-clojure My literature review should bring you up to speed with the relevant details. Typed Clojure is the subject of my undergraduate honours dissertation. http://cloud.github.com/downloads/frenchy64/papers/lit-review%20(1).pdf Happy to elaborate if needed. Thanks, Ambrose On Thu, Jun 21, 2012 at 11:55 AM, cperkins <[email protected]>wrote: > Awhile back I read a short essay by Olin Shivers (*) wherein he observed > that static typing could help the compiler optimize code for the best > performance, check the code for correctness/consistency and also provided a > bit of documentation to the interface of a function. This one activity, > static typing, provides all three benefits. > > But when I revisit the idea with my Rich Hickey inspired glasses on I > think "*is that really a good thing? Isn't it complecting these three > things? Needlessly? And perhaps not doing any one of those tasks as well > or as simply as a something dedicated to one task might*?". > > So taking up the task of insuring correctness/consistency but leaving > aside static typing as is typically practiced. How can we best catch > errors and inconsistencies in our code before our end users do? How can we > do this better than any competing system (like Haskell)? How quickly can > errors be caught - run time, compile time, edit time? > > I don't have answers. I think unit testing has a role, but it's > interesting to try and imagine something that doesn't need unit testing. > Does design-by-contract have a role? Static types and type inference? How > about instead of merely types, using *units* -- like inches and > centimeters -- instead of simply using numbers? How about interval ranges > -- perhaps array reference is limited (at edit time or at compile time) to > the range of 0 to (1- array-length), and any variable passed as an array > index must be inferred to be within that range or an error is thrown by the > correctness checker. And shouldn't the context of a conditional change a > variables type? Example: (when (< 1 x 6) ....) outside that statement > x might just be known to be a number, but inside the body of the when the > correctness checker knowns it is greater than 1 and less than 6. > > I mostly work in Common Lisp and I started a small library to do > consistency checks based on the usual notion of types. Used some macros to > declare the types succinctly and then collapse back to normal defun. But I > stopped work on it partly because I realized that static types aren't > necessarily what I want. What I want is error and consistency checks that I > can perform whenever desired and require the minimum amount of extra work > to leverage (ideally zero extra work). > > Anyway, if anyone has done work in this area or has interesting ideas, > etc. I'd love to discuss them. > > Thanks, > > Chris > > > (*) I can't find this essay now, hopefully I'm not mis-remembering or > mis-attributing it. > > -- > You received this message because you are subscribed to the Google > Groups "Clojure" group. > To post to this group, send email to [email protected] > Note that posts from new members are moderated - please be patient with > your first post. > To unsubscribe from this group, send email to > [email protected] > For more options, visit this group at > http://groups.google.com/group/clojure?hl=en -- You received this message because you are subscribed to the Google Groups "Clojure" group. To post to this group, send email to [email protected] Note that posts from new members are moderated - please be patient with your first post. To unsubscribe from this group, send email to [email protected] For more options, visit this group at http://groups.google.com/group/clojure?hl=en
