3 ms·

Doesn't anyone view static typing as done in a language like Haskell as a form of documentation? I am not saying ALL Haskell code can be deciphered by its type

Doesn't anyone view static typing as done in a language like Haskell as a form of documentation? I am not saying ALL Haskell code can be deciphered by its types - hell no. But a useful technique is to express the semantics of the program into the type system (as much as possible anyways) to communicate intent. This is a huge benefit over dynamic languages imho. So there is more too it than just verification, even if that is extremely nice.

tikhonj 14y ago
This is actually a rather underrated property of good static type systems. Some types (like (a, b) -> a or a -> b -> a) are actually so constraining, they can only have one valid (e.g. not ⊥) implementation. There is actually a program that, given a type signature, can write the trivial function for you [1]. It's pretty awesome, but admittedly more a curio than anything practical. [1]: http://lambda-the-ultimate.org/node/1178 http://lambda-the-ultimate.org/node/1178 Happily, there are practical programs that take advantage of the types' expressiveness. My favorite example: Hoogle[2]. It's brilliant: a search engine that given a type signature gives you a list of functions either with that type (modulo renaming) or a similar type. The beauty is that it can work even if the function is more general than what you're looking for and has a weird name (so a normal search would not be very helpful). [2]: http://www.haskell.org/hoogle/ http://www.haskell.org/hoogle/ A perfect example: let's say you're looking for the equivalent of JavaScript's join method. It would have the type [String] -> String -> String. Now, this particular function does not actually exist in Haskell. Instead, there is a more general function called intercalate that works on any list. Moreover, intercalate's arguments are reversed: it's type is actually [a] -> [[a]] -> [a] (or String -> [String] -> String if made specific to String). And yet, if you search for [String] -> String -> String, the second result is intercalate! It's magical. In short: types are basically a form of self-documenting code, so you get a lot of cool stuff for free given a good type system.
stonemetal 14y ago
In some way yes, but in general not really. (+),(-), (*) all have the type (Num a) a -> a -> a abs, signum both have the type (Num a) a-> a In the first case it works as documentation because I already know what they do. In the second case I read signum as sig num instead of sign num, and was left scratching my head as to what a signature number was, until I read the actual documentation. So I would say types make a good reference documentation but not a good learning documentation. Contrast this with python doc strings which can be both a good reference and a decent source of learning.
gtani 14y ago
GHC/Haskell is edging towards what could be called weak dependent typing or type-level programming, look at Weirich deck and phantom types: http://www.cis.upenn.edu/~sweirich/plmw12/Slides/plmw12-Pierce.pdf http://www.cis.upenn.edu/~sweirich/plmw12/Slides/plmw12-Pier... http://www.haskell.org/haskellwiki/Phantom_type http://www.haskell.org/haskellwiki/Phantom_type http://stackoverflow.com/questions/8600692/datatype-promotion-for-dependently-challenged http://stackoverflow.com/questions/8600692/datatype-promotio... For scala: http://groups.google.com/group/scala-internals/browse_frm/thread/a7fa9c6c2a7d3e48/ http://groups.google.com/group/scala-internals/browse_frm/th... http://www.chuusai.com/2012/01/27/type-level-sorting-in-shapeless/ http://www.chuusai.com/2012/01/27/type-level-sorting-in-shap... ------------- SAT and SMT solvers, e.g. in OCaml http://caml.inria.fr/cgi-bin/hump.cgi?contrib=706 http://caml.inria.fr/cgi-bin/hump.cgi?contrib=706 ----------------- I could give a few dozen more examples in these 3 languages, incluindg Coq which is written in C and OCaml, and agda and idris and others, which are written in C and haskell, or compile down to some stage of haskell compilation.

tikhonj 14y ago

This is actually a rather underrated property of good static type systems. Some types (like (a, b) -> a or a -> b -> a) are actually so constraining, they can only have one valid (e.g. not ⊥) implementation. There is actually a program that, given a type signature, can write the trivial function for you [1]. It's pretty awesome, but admittedly more a curio than anything practical. [1]: http://lambda-the-ultimate.org/node/1178 http://lambda-the-ultimate.org/node/1178 Happily, there are practical programs that take advantage of the types' expressiveness. My favorite example: Hoogle[2]. It's brilliant: a search engine that given a type signature gives you a list of functions either with that type (modulo renaming) or a similar type. The beauty is that it can work even if the function is more general than what you're looking for and has a weird name (so a normal search would not be very helpful). [2]: http://www.haskell.org/hoogle/ http://www.haskell.org/hoogle/ A perfect example: let's say you're looking for the equivalent of JavaScript's join method. It would have the type [String] -> String -> String. Now, this particular function does not actually exist in Haskell. Instead, there is a more general function called intercalate that works on any list. Moreover, intercalate's arguments are reversed: it's type is actually [a] -> [[a]] -> [a] (or String -> [String] -> String if made specific to String). And yet, if you search for [String] -> String -> String, the second result is intercalate! It's magical. In short: types are basically a form of self-documenting code, so you get a lot of cool stuff for free given a good type system.

stonemetal 14y ago

In some way yes, but in general not really. (+),(-), (*) all have the type (Num a) a -> a -> a abs, signum both have the type (Num a) a-> a In the first case it works as documentation because I already know what they do. In the second case I read signum as sig num instead of sign num, and was left scratching my head as to what a signature number was, until I read the actual documentation. So I would say types make a good reference documentation but not a good learning documentation. Contrast this with python doc strings which can be both a good reference and a decent source of learning.

gtani 14y ago

GHC/Haskell is edging towards what could be called weak dependent typing or type-level programming, look at Weirich deck and phantom types: http://www.cis.upenn.edu/~sweirich/plmw12/Slides/plmw12-Pierce.pdf http://www.cis.upenn.edu/~sweirich/plmw12/Slides/plmw12-Pier... http://www.haskell.org/haskellwiki/Phantom_type http://www.haskell.org/haskellwiki/Phantom_type http://stackoverflow.com/questions/8600692/datatype-promotion-for-dependently-challenged http://stackoverflow.com/questions/8600692/datatype-promotio... For scala: http://groups.google.com/group/scala-internals/browse_frm/thread/a7fa9c6c2a7d3e48/ http://groups.google.com/group/scala-internals/browse_frm/th... http://www.chuusai.com/2012/01/27/type-level-sorting-in-shapeless/ http://www.chuusai.com/2012/01/27/type-level-sorting-in-shap... ------------- SAT and SMT solvers, e.g. in OCaml http://caml.inria.fr/cgi-bin/hump.cgi?contrib=706 http://caml.inria.fr/cgi-bin/hump.cgi?contrib=706 ----------------- I could give a few dozen more examples in these 3 languages, incluindg Coq which is written in C and OCaml, and agda and idris and others, which are written in C and haskell, or compile down to some stage of haskell compilation.