5 ms·

Basically, the idea is that when you branch on a conditional, information is gained. This information may be represented in the type system and used by the comp

by Peaker 14y ago

Basically, the idea is that when you branch on a conditional, information is gained. This information may be represented in the type system and used by the compiler to verify safety, or it can be ignored. If it is ignored, the language is said to have "boolean blindness". Example: if (ptr == NULL) { ... a ... } else { ... b ... } In branch a and branch b, different invariants about ptr hold. But the language/compiler are not verifying any of these invariants. Instead, consider: data Maybe a = Nothing | Just a This defines a type "Maybe", parameterized by a type variable "a", and it defines two "data constructors" that can make a Maybe value: "Nothing" which contains nothing, and "Just" which contains a value of type "a" inside it. This is known as a "sum" type, because the possible values of the type are the sum of all data constructor values. We could still use this sum data-type in a boolean-blind way: if isJust mx then .. use fromJust mx .. -- UNSAFE! else .. can't use content of mx .. However, using pattern-matching, we can use it in a safe way. Assume "mx" is of type "Maybe a": case mx of Nothing -> ... There is no value of type "a" in our scope Just x -> ... "x" of type "a" is now available in our scope! So when we branch on the two possible cases for the "mx" type, we gain new type information that gets put into our scope. "Maybe" is of course a simple example, but this is also applicable for any sum type at all. If your language does branching without giving you back any new type information, it means you have to manually track the invariants and conditionals your program is in. If you get it wrong, your program will die at runtime. Instead, the language can almost always provide you some kind of proof that you can pass along of the conditional's truthness, which makes it safe to rely on it.

zemo 14y ago
I may be mistaken, but I believe type switches in Go address this criticism: type Fruit struct { Name string Species string } // define a method on Fruit structs named Rename func (f *Fruit) Rename(s string) { f.Name = s } type Candy struct { Name string Company string } // define a method on Candy structs named Rename func (c *Candy) Rename(s string) { c.Name = s } // any type that defines a method named Rename is also // of type Renamable. type Renamable interface { Rename(string) } // produce something that implements Renamable. Its // fields will be unknown, but the method Rename will be // known to exist. func SomeProducer(...) Renamable { ... } x := SomeProducer(...) // at this point, x is of type Renamable. We do not // know what fields it has. The only thing we know is // that it has some method named Rename that takes a // single string for its only argument and returns // nothing. switch t := x.(type) { case Fruit: // T is of type Fruit, while x is of type Renamable fmt.Print(t.Species) case Candy: // T is of type Candy, while x is of type Renamable fmt.Print(t.Company) default: // some other type. } it's in the Switch section of the Go spec: http://golang.org/ref/spec#Switch_statements http://golang.org/ref/spec#Switch_statements
- AnswerAndForget 14y ago
  Not exactly. You see, you have to define new types from scratch with your approach. With Haskell's approach, you just have to use the Maybe parametric type, which just needs to be defined once. In other words, you just go and use a generic type instead of writing your own, like new List<Integer> instead of new ListInteger in Java.
  - zemo 14y ago
    unless I'm missing something, that seems to address a separate difference in the specifics of Go and Haskell's type systems, namely that Go's interfaces and Haskell's sum types are different. Yes, they're different. I really only meant to say that the article is predicated on the notion that we're only able to branch on booleans instead of predicates. As for checking for null values... var x *MyType ... switch x { case nil: // blah default: // blah } tada, no boolean required, no having to "establish the provenance" of any bits. Sure, inside the nil case, the compiler doesn't actually stop you from unsafely attempting to access the fields of x, and, in that way, Haskell is safer than Go. I'm not trying to assert that Go is better than Haskell or that they are the same; I've never programmed Haskell so I'm not qualified to make such a statement. I'm merely addressing the specific "Boolean Blindness" criticism. I don't really think that criticism is in any way valid, since "Boolean Blindness" isn't a criticism of a language design, it's a criticism of how one might use a particular language. To say that Go committed "Boolean Blindness" is predicated on the following assumptions: - you can only branch on a boolean - given a value and a type, the only thing you can do is obtain a boolean indicating whether or not that value is of that type as far as Go is concerned, those statements are factually inaccurate. Given some variable `x` of unknown type, and a type `t`, is there some way, in Haskell, to create a boolean `v` such that the value of `v` is `true` when `x` is of type `t` and `false` otherwise? And if so, is there some way to branch on this boolean value `v`? Because if that is true, then how has Haskell not committed the same atrocity of "Boolean Blindness"?
    - Peaker 14y ago
      > tada, no boolean required, no having to "establish the provenance" of any bits. Sure, inside the nil case, the compiler doesn't actually stop you from unsafely attempting to access the fields of x, But you do have to establish the provenance of your conditional. You have to keep track of whether you compared against nil yourself. Whether this is expressed as if(x != nil) or as a boolean-blind switch case, the information is lost and it is up to the user to keep track of the meaning of 'x' under all the conditions it is run. Of course Haskell is capable of expressing boolean blind and unsafe code. But Haskell, unlike go is also capable of expressing non-blind, safe code. Go is only able to express boolean blind code (again, it is not about a boolean condition but about whether branching buys you type information). When you compare against nil, it is up to you to keep track of the provenance.
frou_dh 14y ago
Very interesting concept - thanks. It's stuff like this that makes reading comments worthwhile.
drivebyacct2 14y ago
I guess I don't understand the difference between have a typed Go pointer and asking if it is null or not. Nil is nothing, a non-nil value means you can use it. I feel like I'm probably missing a piece of this and I feel dumb about it, sorr I'm not groking it.
- pcwalton 14y ago
  Every time you dereference a pointer in any language with a null pointer type, you're implicitly admitting the chance of a failure (panic, exception, ...). With a sum type (like Maybe or option in ML), you never have this possibility; you have to handle the two cases (null and not-null) separately, and the compiler checks to ensure that you can never use the pointer unless you're in the not-null branch. What Bob Harper is talking about is that, in for example Go, you can write this: if x == nil { ... use x ... } Which is of course a bug. What you meant to write is: if x != nil { ... use x ... } But the Go compiler cannot check this in the general case. However, in ML or Haskell, it's easy. This does not compile, because the type of x will be option<T> instead of T: match x with | None -> ... (* use x *) | Some _ -> () (* do nothing *) But this does compile: match x with | None -> () (* do nothing *) | Some y -> ... (* use y *) Because the type of y will be T instead of option<T>.
  - drivebyacct2 14y ago
    I understand. I guess I don't do even FP to find that to be terribly important to me. To me, and I understand it's not, the pattern matching against None looks to me like a nil check in Go. Also, with your example, the compiler could definitely check, for thread-bound variables, that that code is "incorrect".
    - pcwalton 14y ago
      In the general case, the compiler can't check to see that that code is incorrect. Consider the case in which the boolean result "x == nil" is threaded around from function to function, aliased (you handed out a pointer to it), etc... Also consider the case in which "x" is aliased (you handed out a pointer to it) and it gets mutated to nil in the middle of the branch by calling some function. If you go down this road, you end up making the compiler perform a very difficult (probably undecidable) proof. There has been lots of research on this and it's not easy...
wonderzombie 14y ago
Disclaimer: I love Go and the more I learn about Haskell the more I love it, as well. So is the distinction here that, basically, you push the distinction between a "nothing" and a "something" down into the language layer? IOW, the `if isJust mx` is the programmer trying to reason about a type, whereas `case mx of` is delegating that reasoning to the compiler/language? In general I think that's a good principle, but at least in this example I don't quite grok why `if isJust mx` is out-and-out unsafe. Maybe this is just because the (heh) Maybe example is too simple to illustrate the unsafeness. It does seem more error prone in practice, in terms of engineering & maintenance (read: more likely to lead to bugs). `isJust mx` means you are methodically separating out the verification of what type it is from the access and usage of that type, and since this is all happening at the program layer, you've got to keep the assumptions in your `if` consistent with the assumptions of your type. Conversely the `case of mx` statement leverages the type system to do the work for you. I'll try to put it another way: the code inside your `if isJust` clause is not semantically related to the clause itself except in the most superficial way. However, with `case mx of`, those clauses are inextricably related since you've (again) pushed the semantics of checking the type and unboxing it down a layer, into Haskell. Am I anywhere close?
- Peaker 14y ago
  I may have been slightly misleading if I implied "isJust" is unsafe. It is perfectly safe. What's unsafe is "fromJust" which crashes at runtime if the Maybe value is in fact a Nothing. "isJust" is code-smell because it means you're likely to need a "fromJust" later. The problem is: What if the condition is changed later? What if you use "fromJust" in the else branch? What if the code is moved around outside of the condition's scope? The above is meant to illustrate that the "isJust/fromJust" anti-pattern is out-and-out unsafe. You get no compile-time assurances. If you avoid "fromJust" altogether (and equivalent constructs, of course), you have a 100% guarantee that you will not crash from expecting a Just where there's a Nothing (IOW, nil dereference). Additionally, "Just" and "Nothing" are data constructors (can be viewed as value tags) within the Maybe type, they are not "types" themselves. Except for these points, I think you are generally describing it correctly. This kind of thing (avoiding boolean blindness) as well as a few more safety nets in Haskell is the reason lots of Haskell code is said to Just work once it compiles.

by Peaker 14y ago

zemo 14y ago

I may be mistaken, but I believe type switches in Go address this criticism: type Fruit struct { Name string Species string } // define a method on Fruit structs named Rename func (f *Fruit) Rename(s string) { f.Name = s } type Candy struct { Name string Company string } // define a method on Candy structs named Rename func (c *Candy) Rename(s string) { c.Name = s } // any type that defines a method named Rename is also // of type Renamable. type Renamable interface { Rename(string) } // produce something that implements Renamable. Its // fields will be unknown, but the method Rename will be // known to exist. func SomeProducer(...) Renamable { ... } x := SomeProducer(...) // at this point, x is of type Renamable. We do not // know what fields it has. The only thing we know is // that it has some method named Rename that takes a // single string for its only argument and returns // nothing. switch t := x.(type) { case Fruit: // T is of type Fruit, while x is of type Renamable fmt.Print(t.Species) case Candy: // T is of type Candy, while x is of type Renamable fmt.Print(t.Company) default: // some other type. } it's in the Switch section of the Go spec: http://golang.org/ref/spec#Switch_statements http://golang.org/ref/spec#Switch_statements

AnswerAndForget 14y ago
Not exactly. You see, you have to define new types from scratch with your approach. With Haskell's approach, you just have to use the Maybe parametric type, which just needs to be defined once. In other words, you just go and use a generic type instead of writing your own, like new List<Integer> instead of new ListInteger in Java.
- zemo 14y ago
  unless I'm missing something, that seems to address a separate difference in the specifics of Go and Haskell's type systems, namely that Go's interfaces and Haskell's sum types are different. Yes, they're different. I really only meant to say that the article is predicated on the notion that we're only able to branch on booleans instead of predicates. As for checking for null values... var x *MyType ... switch x { case nil: // blah default: // blah } tada, no boolean required, no having to "establish the provenance" of any bits. Sure, inside the nil case, the compiler doesn't actually stop you from unsafely attempting to access the fields of x, and, in that way, Haskell is safer than Go. I'm not trying to assert that Go is better than Haskell or that they are the same; I've never programmed Haskell so I'm not qualified to make such a statement. I'm merely addressing the specific "Boolean Blindness" criticism. I don't really think that criticism is in any way valid, since "Boolean Blindness" isn't a criticism of a language design, it's a criticism of how one might use a particular language. To say that Go committed "Boolean Blindness" is predicated on the following assumptions: - you can only branch on a boolean - given a value and a type, the only thing you can do is obtain a boolean indicating whether or not that value is of that type as far as Go is concerned, those statements are factually inaccurate. Given some variable `x` of unknown type, and a type `t`, is there some way, in Haskell, to create a boolean `v` such that the value of `v` is `true` when `x` is of type `t` and `false` otherwise? And if so, is there some way to branch on this boolean value `v`? Because if that is true, then how has Haskell not committed the same atrocity of "Boolean Blindness"?
  - Peaker 14y ago
    > tada, no boolean required, no having to "establish the provenance" of any bits. Sure, inside the nil case, the compiler doesn't actually stop you from unsafely attempting to access the fields of x, But you do have to establish the provenance of your conditional. You have to keep track of whether you compared against nil yourself. Whether this is expressed as if(x != nil) or as a boolean-blind switch case, the information is lost and it is up to the user to keep track of the meaning of 'x' under all the conditions it is run. Of course Haskell is capable of expressing boolean blind and unsafe code. But Haskell, unlike go is also capable of expressing non-blind, safe code. Go is only able to express boolean blind code (again, it is not about a boolean condition but about whether branching buys you type information). When you compare against nil, it is up to you to keep track of the provenance.

frou_dh 14y ago

Very interesting concept - thanks. It's stuff like this that makes reading comments worthwhile.

drivebyacct2 14y ago

I guess I don't understand the difference between have a typed Go pointer and asking if it is null or not. Nil is nothing, a non-nil value means you can use it. I feel like I'm probably missing a piece of this and I feel dumb about it, sorr I'm not groking it.

pcwalton 14y ago
Every time you dereference a pointer in any language with a null pointer type, you're implicitly admitting the chance of a failure (panic, exception, ...). With a sum type (like Maybe or option in ML), you never have this possibility; you have to handle the two cases (null and not-null) separately, and the compiler checks to ensure that you can never use the pointer unless you're in the not-null branch. What Bob Harper is talking about is that, in for example Go, you can write this: if x == nil { ... use x ... } Which is of course a bug. What you meant to write is: if x != nil { ... use x ... } But the Go compiler cannot check this in the general case. However, in ML or Haskell, it's easy. This does not compile, because the type of x will be option<T> instead of T: match x with | None -> ... (* use x *) | Some _ -> () (* do nothing *) But this does compile: match x with | None -> () (* do nothing *) | Some y -> ... (* use y *) Because the type of y will be T instead of option<T>.
- drivebyacct2 14y ago
  I understand. I guess I don't do even FP to find that to be terribly important to me. To me, and I understand it's not, the pattern matching against None looks to me like a nil check in Go. Also, with your example, the compiler could definitely check, for thread-bound variables, that that code is "incorrect".
  - pcwalton 14y ago
    In the general case, the compiler can't check to see that that code is incorrect. Consider the case in which the boolean result "x == nil" is threaded around from function to function, aliased (you handed out a pointer to it), etc... Also consider the case in which "x" is aliased (you handed out a pointer to it) and it gets mutated to nil in the middle of the branch by calling some function. If you go down this road, you end up making the compiler perform a very difficult (probably undecidable) proof. There has been lots of research on this and it's not easy...

wonderzombie 14y ago

Disclaimer: I love Go and the more I learn about Haskell the more I love it, as well. So is the distinction here that, basically, you push the distinction between a "nothing" and a "something" down into the language layer? IOW, the `if isJust mx` is the programmer trying to reason about a type, whereas `case mx of` is delegating that reasoning to the compiler/language? In general I think that's a good principle, but at least in this example I don't quite grok why `if isJust mx` is out-and-out unsafe. Maybe this is just because the (heh) Maybe example is too simple to illustrate the unsafeness. It does seem more error prone in practice, in terms of engineering & maintenance (read: more likely to lead to bugs). `isJust mx` means you are methodically separating out the verification of what type it is from the access and usage of that type, and since this is all happening at the program layer, you've got to keep the assumptions in your `if` consistent with the assumptions of your type. Conversely the `case of mx` statement leverages the type system to do the work for you. I'll try to put it another way: the code inside your `if isJust` clause is not semantically related to the clause itself except in the most superficial way. However, with `case mx of`, those clauses are inextricably related since you've (again) pushed the semantics of checking the type and unboxing it down a layer, into Haskell. Am I anywhere close?

Peaker 14y ago
I may have been slightly misleading if I implied "isJust" is unsafe. It is perfectly safe. What's unsafe is "fromJust" which crashes at runtime if the Maybe value is in fact a Nothing. "isJust" is code-smell because it means you're likely to need a "fromJust" later. The problem is: What if the condition is changed later? What if you use "fromJust" in the else branch? What if the code is moved around outside of the condition's scope? The above is meant to illustrate that the "isJust/fromJust" anti-pattern is out-and-out unsafe. You get no compile-time assurances. If you avoid "fromJust" altogether (and equivalent constructs, of course), you have a 100% guarantee that you will not crash from expecting a Just where there's a Nothing (IOW, nil dereference). Additionally, "Just" and "Nothing" are data constructors (can be viewed as value tags) within the Maybe type, they are not "types" themselves. Except for these points, I think you are generally describing it correctly. This kind of thing (avoiding boolean blindness) as well as a few more safety nets in Haskell is the reason lots of Haskell code is said to Just work once it compiles.