7 ms·
Brilliance of Haskell's Maybe type and the Value of Static Type Checking
- tkahn6 16y agoThis is probably a good place to share www.brics.dk/~hosc/local/LaSC-8-4-pp293-341.pdf The first 11 pages really helped me understand the motivations for monads and it explains bind and return. It's written really clearly and doesn't assume much prior knowledge. I think it may be the original paper introducing monads to Haskell but I could be wrong. (For some reason its a .pdf when it should be .ps.gz)
- jewbacca 16y agoLink to Simon PJ's own copy, with accurate extension: http://research.microsoft.com/en-us/um/people/simonpj/papers/state-lasc.ps.gz http://research.microsoft.com/en-us/um/people/simonpj/papers...
- delackner 16y agoI got to page 8, where he introduces an upside-down A as I guess a symbol meaning "the set of all" and do not understand even after three readings, anything that is said on page 9.
- celoyd 16y agoYou guessed pretty much right: ∀ is usually read as for all. It and others he uses (like ⊢ for is derived from) are defined in http://en.wikipedia.org/wiki/List_of_logic_symbols http://en.wikipedia.org/wiki/List_of_logic_symbols . Hope that helps; as a beginner in Haskell and strong type systems, it looks like I’m going to have trouble with this too.
- ionfish 16y ago∀ is the standard symbol for the universal quantifier: some proposition is true for all elements in the universe being quantified over. This is stated explicitly in the paper: "The type given for runST above is implicitly universally quantified over both s and a." We could thus expand the type given for runST as follows: runST is a function which, for every instance of the type a, and every instance of the type s, accepts a state transformer (with type ST s a) and returns a value of type a. If you want to attain a better understanding of the logical concepts and notation used in the article, try getting hold of an introductory logic text. I recommend Enderton's 'A Mathematical Introduction to Logic'. http://www.math.ucla.edu/~hbe/amil/index.html http://www.math.ucla.edu/~hbe/amil/index.html
- delackner 16y agoBoth your and the previous reply indicate that the blanks I filled in (the "for all" and "derived from" symbols) were indeed as I suspected, and yes I understood the definition of runST to be as you describe it. But I still don't comprehend their discussion of how defining runST thusly somehow provides safety in the example they say it would automatically detect is disallowed.
- Zak 16y agoI've always thought it bizarre that many languages with static typing allow arbitrary values to be null. It's par for the course with dynamic typing, of course. Damn you, C.A.R. Hoare!
- tome 16y agoHe did apologise for it: http://en.wikipedia.org/wiki/C._A._R._Hoare#Quotes http://en.wikipedia.org/wiki/C._A._R._Hoare#Quotes
- _delirium 16y agoIt's a common design change in C dialects, but none seem to have really caught on. For example, Cyclone has both nullable and non-nullable pointers (http://cyclone.thelanguage.org/wiki/Cyclone%20for%20C%20Programmers#Pointers http://cyclone.thelanguage.org/wiki/Cyclone%20for%20C%20Prog...).
- eelco 16y agoI like Objective-C's solution, where one can just send messages to nil. The practical result when writing code is pretty close to using the Maybe monad applicatively (i.e., write your code like the value is never nil, only check for nil when it's part of the (bigger) logical flow in your code.)
- masklinn 16y agoThe problem is that, though operations flow better, it's a good way to hide bugs until you've completely lost its context, and then finding out its source is a pain unless you have a backtracking debugger. An option type, especially one which allows you to lift operations into it (as Haskell's does) is a much better solution as it gives the programmer the choice of behavior: does he not care and just want to keep his option, or does he want to know and unwrap the value within the container? Objective-C allows half of this, but it's generally the wrong half. Most other statically typed languages allow neither solution and are therefore broken.
- sunkencity 16y agoIn ruby of course you have raganwald's andand which is sort of the same as the maybe monad. It should really be built into the language like in haskell I think (and be allowed a shorter name, like .&& or maybe something else that doesn't upset the parsing). http://github.com/raganwald/andand http://github.com/raganwald/andand
- jrockway 16y agoMaybe is not built into Haskell. Haskell has syntax sugar that turns do { x <- foo; bar x } into "foo >>= \x -> bar x" for any Monad. Maybe is just a particular instance of Monad that is included in the Prelude. But you can write your own that is exactly identical in every way.
- _delirium 16y agoI guess I'm missing what's specifically monadic about it. Isn't it just an algebraic data type with two alternatives? In ML you declare the morally-equivalent "option" type as: datatype 'a option = NONE | SOME of 'a It's possible that the Haskell Maybe monad is doing some additional magic, but I didn't get that from this article if so (does it have something that lets you avoid manually pattern-matching on the two cases and/or using accessors?).
- vito 16y agoJust 1 >> Nothing >> Just 3 => Nothing Just 1 >> Just 2 >> Just 3 => Just 3 To answer your last question, yes. It basically adds short-circuiting.
- naradaellis 16y agoA monad is just a container with some operations to work indirectly with its contents.
- deleted 16y ago[deleted]
- raganwald 16y agoI don't know why the author mentioned that Ruby allows any value to be null. Languages like Ruby and Javascript don't have static type checking, therefore their handling of null "not even wrong" compared to Haskell and OCaml which allow you to have the compiler eliminate null pointer exceptions at run time. IIRC, some Java dialects re-introduce the idea of a variable that cannot be null, and it is possible to do fancy tricks with annotations to produce the same effect.
- Chirono 16y agoAlthough you eliminate null pointer exceptions, lazy evaluation does introduce another subtle and very similar class of errors. Consider a program that takes a leaf-labelled tree of Ints and replaces each int with the maximum found in the whole tree. You can do this in two passes over the tree - one to find the max value, one to re-write the tree. But you can also do it in a single pass using lazy evaluation: ---------------- data Tree = Branch Tree Tree | Leaf Int label :: Tree -> Tree label tree = t2 where (t2,k) = thread tree k thread :: Tree -> Int -> (Tree,Int) thread (Leaf v) k = (Leaf k, v) thread (Branch l r) k = (Branch l' r', max lv rv) where (l',lv) = thread l k (r',rv) = thread r k ---------------- The idea here is that `thread` runs through the tree replacing the values with some input value `k` and also calculates the max value of the tree. The function `label` then uses the output of thread as its own input. This all works fine as long as you never look at the value of `k` inside `thread`. If you do, you go into an infinite loop as `k` then depends on itself. This is similar to `k` being a pointer to an Int that doesn't get initialised until the function `thread` returns. If you examine it before then, you get a null pointer exception.
- masklinn 16y ago> Although you eliminate null pointer exceptions, lazy evaluation does introduce another subtle and very similar class of errors. But those are completely different features, option types don't imply lazy evaluation (and the other way around). OP didn't talk about lazy evaluation once. There might be issues with lazy eval, but that's completely not the subject.
- deleted 16y ago[deleted]
- Chirono 16y agoYeah, I know they aren't related. I just thought it might be interesting to show that this kind of bug can still crop up even without nullable types. So the statement made at the end of the post doesn't quite hold: > In Haskell, it is simply impossible to write a program that is susceptible to NullPointerExceptions at runtime unless you explicitly make the type in question optional by wrapping with Maybe. That said, lazy knot-tying isn't something you tend to write by accident. You generally know that it's going on.
- iman 16y agoThere is a story that one of the designers of Java was pushing very hard in favour of Java references being non-nullable by default. But Gosling rejected the idea claiming that it would be too confusing for programmers and it would kill any chances of Java achieving popularity. Here is a relevant paper, "Non-null References by Default in Java: Alleviating the Nullity Annotation Burden": http://www.springerlink.com/content/f197143t80671627/ http://www.springerlink.com/content/f197143t80671627/ "we conducted an empirical study of 5 open source projects (including the Eclipse 3.3 JDT Core) totaling over 700 KLOC. The results allow us to confirm that in Java programs, at least 2/3 of declarations of reference types are meant to be non-null, by design."
- masklinn 16y ago> There is a story that one of the designers of Java was pushing very hard in favour of Java references being non-nullable by default. But Gosling rejected the idea Is there a source for that? And has Gosling apologized to the world since then? (I mean Hoare apologized, Gosling should grovel and beg for forgiveness)
- iman 16y agoI don't have a source and I don't quite remember where I heard it. It's probably not true. Although this post from Lambda the Ultimate mentions a similar sentiment: http://lambda-the-ultimate.org/node/1905#comment-23217 http://lambda-the-ultimate.org/node/1905#comment-23217
- masklinn 16y agoIt's still a bit weird, I think: a lot of the migration to Java was from enterprise C++, and while C++ has null pointers it doesn't have null references. So that wouldn't have been much of a change.
- JulianMorrison 16y agoThis could be fixed in Java by two simple changes. x = func(null); // func is ignored and x is null proc(null); // proc is ignored and an NPE is thrown. and so implicitly y = a(b(c(d(null)))); // a b c d are ignored and y == null This would mean you could treat null like Nothing, threading it through non side effecting functions and only testing the result. If you tried to use it with a side effect, it would halt. The compiler would be free to omit these checks where x is provably not null. For example: foo (x); y = bar(x); The assignment to y does not need a null check, because a null would have thrown NPE in foo. Side effect of this design: code will never receive a null in parameters. Parameter values can be assumed to be definitely not-null by coder and compiler alike. EDIT: one more change would be needed: prim = func(ref) is illegal unless ref can be proved not null. Also, add a no-op built-in, notnull(x) that does nothing except NPE if x is null. That could be used as proof to the compiler.
- masklinn 16y agoThis is an utterly terrible idea. Acceptable — barely — in dynamically typed languages, but utterly moronic for a strongly typed language where you can make references null-safe statically and at the type level. Hiding nulls under the carpet is only a recipe for painfully hard to discover bugs in the long run.
- JulianMorrison 16y agoThis design is type level. Properties and primitives are not null, references used after a guard procedure are not null, other references are Maybe types. Functions are Maybe typed if they are operating on nullable references. Those types are not syntactically top level, but that's because I was considering an alteration, not a rewrite.
- oozcitak 16y ago> Languages like Java, Ruby, and C# all make the mistake of allowing any type at all to hold null. Just a little nitpicking here. In C# integral types cannot hold null unless explicitly declared nullable [1], ie. int x = null; // won't compile int? x = null; // compiles fine, shorthand for Nullable<int> x = null; I wish this was the default behavior for reference types, too. [1]: http://msdn.microsoft.com/en-us/library/1t3y8s4s(VS.80).aspx http://msdn.microsoft.com/en-us/library/1t3y8s4s(VS.80).aspx