5 ms·

Backed. Optional typing seems really promising, I'd like to hear more about what kinds of things it can't do though. If you hypothetically do annotate all you

• rayiner 13y ago
  It depends on the particular type system. For example in Dylan or Common Lisp (or Dart), annotating all types doesn't guarantee anything about whether you can still have type errors at runtime. In typed-clojure or typed-racket, you have a guarantee that if a type error does happen, it will happen either in dynamically-typed code, or on the boundary between dynamically and statically typed code.
• ambrosebs 13y ago
  Thanks. There are certainly important tradeoffs. Haskell the language and Haskell the type system are designed to prevent many kinds of programming mistakes. Typed Clojure is designed to follow any decisions Clojure makes. For example, it's not a type error to lookup a nonexistent key in a map, so we can't really catch typos in keys. Clojure allows dynamic code loading, so it would be rather fruitless to try completeness checking (and languages like Haskell can do it so much better). You might want to watch my 2012 Clojure Conj talk. I think it touches briefly on this issue. I've always tried to be upfront about the limitations of Typed Clojure. I apologise if that was a bit rambly, it's 5AM :)
• brandonbloom 13y ago
  > kinds of things it can't do The most obvious thing an optional type system can't do is perform implicit searches that affect the semantics of the resulting program. Many of us consider this to be a good thing! > what are you missing out on by not having pervasive static typing built in like in Haskell One example of an implicit search is Haskell's return type polymorphism, where overloading is resolved by solving a logic puzzle to find a function with an unambiguous type signature match. You can get around this problem statically or dynamically: Statically #1: Explicit Search Although probably overkill for something like resolving "read" to "readInteger" vs "readFloat", you can invoke a logic engine on a piece of code. This means that your language needs to support staging constructs, so that you can run code at various "times". Macros give us this, but there are potentially better mechanisms. You'll also need first class representations of previous loaded code, code under observation, the type solver, etc. People do things like this with core.logic in Clojure now: They generate a data structure, solve something about it, then either generate code from the solution or interpret some annotated data structure. Statically #2: Explicit Parameterization Just be explicit and write readFloat instead of read! If you need your code to be generic, you can use macros etc to fill in that slot at compile time. Dynamically: OOP Techniques See "Existential Types". As long as your coding to interfaces instead of concrete types, you can create proxy objects who can perform dynamic dispatch. What is a search problem at compile time is often a key lookup at runtime. This is what happens behind the scenes with generic monad code in GHC and friends anyway: They reify a dictionary of methods and thread that through.
• tikhonj 13y ago
  Yes, there are differences. Fundamentally, the Haskell type system is not just about correctness: it actually makes the language more expressive! You simply wouldn't be able to do some very awesome typeclass things with a system like this, for example. I've found things like QuickCheck--or even just using different monads--to be much more awkward without typeclasses. The way this works is by allowing you to overload a function on its return type. It's very easy to imagine a function overloaded on its argument; for example, a hypothetical: to_string :: a -> String This function can take an argument of some sort and returns its string representation. Many languages support this sort of overloading--it's very straightforward. But what about the symmetric from_string function? from_string :: String -> a Now this is trickier! Most languages would force you to be more explicit about which function you're using, so you would have to write something like Double.from_string or Integer.from_string and so on. This loses the symmetry inherent in the types and forces you to add a whole bunch of redundant noise to your code. Very reminiscent of Java's Foo i = new Foo()! With typeclasses, you can actually write a from_string function like this. Moreover, it works using exactly the same type inference system you already know and love! In practice, this means that the overloading is very straighforward: it just chooses whatever type you need. And since the type system is pervasive, you know that it will always choose the right instance if possible: if you use from_string expecting an int, it can't accidentally use Float.from_string because that wouldn't even typecheck. This turns out to be useful in a whole bunch of different places. One of my favorites is with numeric literals: in Haskell, numeric literals are polymorphic. This means that if you write f 10, 10 will be the right type--integer, double, arbitrary precision integer, whatever--for the function. No more arbitrary sigils after your numbers (like 10L). More importantly, this makes new numeric types feel just like native ones[1]. So you can use normal literals with rational numbers or constructive real numbers or 8-bit words or symbolic bitvectors (most of which I've used in real code). These types no longer feel like second-class citizens! Haskell type inference is even more useful than that though. Not only does it reduce the burden of using the type system, it also actually enables new workflows. Instead of giving the compiler your types and waiting for it to show you where they're wrong, you can actually just ask the compiler what type it expects. You can use this to interactively grow your program, informed by your types. The newest version of GHC will make this more convenient by adding a feature called "type holes", which lets you leave holes in your code and will tell you the types of those holes. Once this gets good editor support, it'll be incredible. The Haskell type system--partly because it's pervasive and partly because it controls effects--also makes some high-level optimizations like steam fusion possible. The basic idea is that it can rewrite multiple logical traversals over an array into a single tight loop. The crazy thing is that this optimization is actually specified by a library, and not built into the compiler! So there are actually a whole bunch of rewrite optimizations like this, most of which are only guaranteed to be correct thanks to the type system. Since they're somewhat tricky to debug even with all the existing guarantees, I don't even want to imagine what it would be like with a weaker type system. Honestly, I think you would be missing out on most of the real advantages Haskell gives you. And for what? At least in my experience, you do not get much of a boost in productivity or expressiveness. Even without invoking the optional type system. So yeah: lots of deeper tradeoffs. [1]: Take a look at "Growing a Language", a brilliant talk by Guy Steele that goes into why it's important to allow new additions to feel just like native parts of a language. http://www.youtube.com/watch?v=_ahvzDzKdB0 http://www.youtube.com/watch?v=_ahvzDzKdB0