People in the Haskell community get awfully excited about Haskell's type system. When I was first learning Haskell, I found this rather odd. After all, a "type" is just a flat name that tells the compiler how many bits to allocate and which operations to allow, right? As I read further, I quickly discovered that in Haskell, the type system is something much more powerful. In a normal language, the type system prevents you from accidentally trying to multiply a string by a binary tree of integers, or pass a function an signed integer when it's expecting an unsigned integer. But in Haskell, the combination of parametric polymorphism, typeclasses and automatic type inference combine to form a potent mixture. Even without any exotic language extensions, in Haskell you can use the type system to *prove stuff about your programs*! And not necessary stuff that's anything to do with the usual notion of a "data type". You can prove that lists are non-empty or even of a specific size. You can prove that optional values get checked before they are used. And you can prove that user input is sanitised before being passed to sensitive functions. (Or rather, you can make your program simply not compile if the required properties are not guaranteed.) Let's take an example. Suppose you have some functions that obtain input from a user, and you have some other functions that do something with this data. What you can do is something like this: newtype Data x y = Data x data Checked data Unchecked check_string :: Data String Unchecked -> Data String Checked Now make it so that everything that obtains data from the user returns Data String Unchecked, and everything that uses a string to do something potentially hazardous demands Data String Checked. (And any functions that don't care whether the string is checked or not can just use Data String x.) Only one problem: Any functions that expect a plain String now won't work. Particularly, the entirity of Data.List will refuse to accept this stuff. Which is kind of galling, considering that a Data String Checked *is* a String! What we're really trying to do here is attach additional information to a value - information which exists only in the type checker's head, but has no effect on runtime behaviour (other than determining whether we *get* to runtime). As far as I can tell, Haskell does not provide any way to take an existing type and attach additional information to it in such a way that code which cares about the new information can make use of it, but existing code which doesn't care continues to work. Any comments on this one? On a rather unrelated note, I found myself thinking about the Type Families extension (or whatever the hell it's called). I found that I can do this: class Collection c where type Element c :: * empty :: c first :: c -> Maybe (Element c) ... This works for collections that can contain *anything*: instance Collection [x] where type Element [x] = x ... It works for collections that can only contain *one* type: instance Collection ByteString where type Element ByteString = Word8 ... And it works for collections that can handle more than one type, but less than *every* type: instance Ord x => Collection (Set x) where type Element (Set x) = x ... Something quite interesting is happening here: this "Element" thing is almost like a *function* which takes one type and returns another. A function that operates on types themselves. Now suppose I want to write a function that converts one kind of collection into another: convert :: (Collection c1, Collection c2) => c1 -> c2 Erm, no. That doesn't work AT ALL. What we want to say is that the element types are constrained (specifically, they're identical). I searched for quite some time looking for a way to say this. In the end, I gave up and let the compiler deduce the type signature automatically. Apparently the correct signature is convert :: (Collection c1, Collection c2, Element c1 ~ Element c2) => c1 -> c2 Apparently the bizare syntax "Element c1 ~ Element c2" means that these two types are supposed to be equal. (Why not just an equals sign?) This got me thinking... Maybe what we'd really like to say is something like convert :: (Collection c1 {Element = x}, Collection c2 {Element = x}) => c1 -> c2 In other words, make the assosiated type like a named field of the class, using syntax similar to the named fields that values can have. And then, if we can do it to classes, why not types? data Map {keys :: *, values :: *} = ... insert :: (Ord k) => k -> v -> Map {keys = k, values = v} -> Map {keys = k, values = v} Now, it seems reasonable that if one of the type fields is unconstrained, you do not need to mention it: keys :: (Ord k) => Map {keys = k} -> [k] values :: Map {values = v} -> [v] If we can have some mechanism for adding new type fields to an existing type, we are one step away from the problem at the beginning. You could take the existing String type, and add (by whatever the mechanism is) a new "safety" field to it. All of Data.List ignores this field, but any new code you write can choose to use it if required. At least, that's my vague idea. Anybody like it? (My first thought is that "Map {keys = k, values = v}" is going to start getting tedious to type very, very quickly. Perhaps we should do something like values :: (m :: Map {values = v}) => m -> [v], or even allow values :: (m :: Map {}) => m -> [values m] as an alternative? IDK.) So there you have it. Multiple paragraphs of semi-directed rambling about type systems. All written by somebody who doesn't even know what a Skolem variable is. :-}