Haskell's type system can also express interesting things most languages' type systems can't.
For example:
https://github.com/yairchu/red-black-tree/blob/master/AvlTre... -- in lines 13..21, an AVLTree type is defined -- with its invariants encoded in the type system. If there's a mistake in these 9 lines, you may get a wrong program. But the nice thing is that if you get just these 9 lines right -- then the hundreds of lines below it that implement an AVL tree cannot get the AVL invariants wrong.
Lines 26..36 inclusive encode the RBTree type such that the invariants are enforced by the type-checker.
In case this is unclear: the type-checker enforcing the correctness of the invariants is at compile-time. A running program is a correct program, at least from the invariants' perspective.
GADT are really cool, but I would like to note three caveats:
1.
> in lines 13..21, an AVLTree type is defined -- with its invariants encoded in the type system
Its balance invariants are encoded, but its ordering invariants are not.
2. The code for manipulating AVL and red-black trees in GADT form is significantly more complicated that it would be if they were not in GADT form.
3. Sometimes, whether using GADTs or not, one ends up with code like this, from the AVL example:
> Nil -> undefined -- shouldnt happen
Needless to say, this negatively affects the comfort we might receive from the type system.
Having said all that, I think there are cases where GADTs are really worth the extra effort. Sometimes, they even simplify code when the alternative to GADTs is checking things at run-time!
1. True, this is harder in Haskell. More easily possible in a language like Agda.
2. The assurances you get in return are probably worth it.
3. I think that piece is unnecessary, and the type system will see that constructor is impossible. If it doesn't, it's a limitation of Haskell GADT's, and can be fixed. I don't think you ever resort to "Nil -> undefined" in Agda.
That's a very interesting question. I made a stab at removing the invariant enforcement from the AVL tree code, but it was more involved than I expected.
In this specific case, it doesn't matter much since compilation takes less than a second on my underpowered netbook. I'm curious whether it's an issue for a program of significant size.
On the one hand, I agree. On the other hand, a type declaration cannot possibly tell you /why/ unless the type system encodes a significant portion of our physical world.
This encoding is left as an exercise for the reader.
Agreed, generally. I'd say comments are to express things the code itself cannot. More expressive languages can get by with good naming, some declarations, and clear idioms in many cases.
The most useful kind of comments are "why" comments, about why specific design trade-offs were chosen.
I mainly agree with you, but for something like that, "it's an AVL tree, look it up" is all it should need. Names and type declarations handle the rest.
If you want to dismiss me as "one of those" people that is anti-commenting, you're reading too much into what I said. You said, "it doesn't have comments!", I said "actually, it does, and they're even checked." The end.
In a more complex program, I'd add comments. How many, and the nature of the comments, depends on whether I was writing in something relatively low-level (like C) or something high-level (like Haskell, Erlang, or K).
Comments
Haskell's type system can also express interesting things most languages' type systems can't.
For example:
https://github.com/yairchu/red-black-tree/blob/master/AvlTre... -- in lines 13..21, an AVLTree type is defined -- with its invariants encoded in the type system. If there's a mistake in these 9 lines, you may get a wrong program. But the nice thing is that if you get just these 9 lines right -- then the hundreds of lines below it that implement an AVL tree cannot get the AVL invariants wrong.
The same is also true for Red Black Trees: https://github.com/yairchu/red-black-tree/blob/master/RedBla...
Lines 26..36 inclusive encode the RBTree type such that the invariants are enforced by the type-checker.
In case this is unclear: the type-checker enforcing the correctness of the invariants is at compile-time. A running program is a correct program, at least from the invariants' perspective.
GADT are really cool, but I would like to note three caveats:
1.
> in lines 13..21, an AVLTree type is defined -- with its invariants encoded in the type system
Its balance invariants are encoded, but its ordering invariants are not.
2. The code for manipulating AVL and red-black trees in GADT form is significantly more complicated that it would be if they were not in GADT form.
3. Sometimes, whether using GADTs or not, one ends up with code like this, from the AVL example:
> Nil -> undefined -- shouldnt happen
Needless to say, this negatively affects the comfort we might receive from the type system.
Having said all that, I think there are cases where GADTs are really worth the extra effort. Sometimes, they even simplify code when the alternative to GADTs is checking things at run-time!
1. True, this is harder in Haskell. More easily possible in a language like Agda.
2. The assurances you get in return are probably worth it.
3. I think that piece is unnecessary, and the type system will see that constructor is impossible. If it doesn't, it's a limitation of Haskell GADT's, and can be fixed. I don't think you ever resort to "Nil -> undefined" in Agda.
How much does this much use of the type system's invariant enforcement increase compilation time? (still just getting into Haskell)
That's a very interesting question. I made a stab at removing the invariant enforcement from the AVL tree code, but it was more involved than I expected.
In this specific case, it doesn't matter much since compilation takes less than a second on my underpowered netbook. I'm curious whether it's an issue for a program of significant size.
This might be beautiful code but come on, not a single comment?
See those type declarations? Those are comments. Comments that are automatically checked.
On the one hand, I agree. On the other hand, a type declaration cannot possibly tell you /why/ unless the type system encodes a significant portion of our physical world.
This encoding is left as an exercise for the reader.
Agreed, generally. I'd say comments are to express things the code itself cannot. More expressive languages can get by with good naming, some declarations, and clear idioms in many cases.
The most useful kind of comments are "why" comments, about why specific design trade-offs were chosen.
<sigh> So you're one of these "Code properly written shouldn't need comments" people, uh?
To understand code, you need to figure out "why" and "what". Code gives you one, comments give you the other.
I mainly agree with you, but for something like that, "it's an AVL tree, look it up" is all it should need. Names and type declarations handle the rest.
If you want to dismiss me as "one of those" people that is anti-commenting, you're reading too much into what I said. You said, "it doesn't have comments!", I said "actually, it does, and they're even checked." The end.
In a more complex program, I'd add comments. How many, and the nature of the comments, depends on whether I was writing in something relatively low-level (like C) or something high-level (like Haskell, Erlang, or K).
You might be assuming a little much about the purpose and target audience of this code :-)
I didn't write it, by the way.
Comments: the great deceivers.
To paraphrase: Some people write tricky code and say, "Ah! I will use a comment to make this clear." Now they have two problems.