lexi-lambda

I think it’s fantastic that Elm works well for you; it’s a wonderful language and there’s no doubt that it is much simpler than Haskell. I agree with you that, in many cases, the technique you’re describing is sufficient, and it requires much less sophisticated machinery than some of the fancier Haskell techniques.

That said, I do think what you’re describing is different from what is described in the blog post. Opaque/abstract types reduce the trusted code significantly, which is fantastic, but the example provided in the blog post is actually even better than that: because NonEmpty is correct by construction, the amount of trusted code goes down to zero. A lot of the tools Haskell provides, like GADTs and type families, can be used to capture more invariants in a correct-by-construction way, rather than relying on abstraction boundaries. There are advantages and disadvantages to both.

I certainly don’t have any ill will toward anyone who finds the complexity of Haskell not worth the extra benefits, so to be quite clear, I’m not trying to sell you on Haskell instead of Elm! I do think being aware of the distinction is still useful, though.

TypeScript is sadly very unsound by design, so doing this kind of thing in TypeScript is always going to be more “best effort” and less “exhaustive proof.” That’s not necessarily wrong or bad per se, as after all, Haskell has escape hatches, too (and so do dependently-typed languages, for that matter). However, there are philosophical differences between the way the languages’ type systems are designed.

When I’ve talked to people who develop and use TypeScript, the general impression I’ve gotten from them is that TS is actually as much about tooling as it is about correctness. TS enables things like autocomplete, jump to definition, and quick access to documentation, and it does that by leveraging the typing information to “see through” the dynamic dispatch that makes that sort of thing infeasible in dynamically-typed JavaScript. The TS type system does provide some correctness benefits, don’t get me wrong, but where ease of use and correctness are in conflict, usually ease of use is preferred.

This is true even with all the “strictness” options enabled, like strict null checking. For some examples of TypeScript unsoundness, see [1] and [2]. Flow is actually generally a lot better than TS in this regard (though it does still have some major soundness holes), but it looks like TS has basically “won,” for better or for worse. But again: TS won because its tooling was better, not because its ability to actually typecheck JS programs was better, which I think reinforces what I said in the previous paragraph on what TS is really about.

[1] https://twitter.com/lexi_lambda/status/1068704405124452352

[2] https://twitter.com/lexi_lambda/status/1068705142109810688

The idea really is that parsing subsumes validation. If you’re parsing, you don’t have to validate, because validation is a natural side-effect of the parsing process. And indeed, I think that’s the very thesis of the blog post: parsing is validation, just without throwing away all the information you learned once you’ve finished!

I have provided a translation of the NonEmpty datatype into Java in this comment: https://news.ycombinator.com/item?id=21478322

However, to answer your “why” question: mostly just because I write Haskell for a living, and my primary personal motivation for writing this blog post was to share with my coworkers and to point to during code reviews. Therefore, it makes the most sense for the examples to be in Haskell! Haskell is also especially well-suited for communicating this sort of thing if you already understand the notation, as you can sort of see from the Java translation: it’s significantly more verbose just to get the same idea across. Still, it’d be great if someone were to provide a “translation” of the same ideas to other languages, no doubt!

I think this is a reasonable point, and your split() example is a good one. I wasn’t sure while I was writing the blog post if I considered isomorphisms to be parsers, and I’m still not entirely sure if I do or not, but there’s an argument to be made that they are simply parsers where the set of possible failures is empty. I don’t have strong feelings about that distinction one way or the other, though.

> You also seem to have missed the point of the Java example anyway, in a misses-the-forest-for-the-trees way.

Perhaps I did, yes. I do think the kind of thing you’re describing is valuable, to be clear. A lot of my comment was intended more as clarification for other people reading these comments than as an argument against what you were saying. I imagine that if I misunderstood your point, other people are likely to, too, so if anything, your clarification is generally a good outcome, I think!

> But the type itself doesn't say that it must return the first element.

Sure, I didn’t say it does. That type isn’t a full specification of head. This blog post isn’t about proving literally everything in your program correct, which is impractical anyway because if you did that it would be as easy to prove the wrong thing as to write a bug in the first place. Some functional tests are still needed.

> Okay, what about more complex cases? E.g. how do you describe type "such value doesn't exist in the db table yet"?

I’ve addressed that kind of question more generally in another comment[1], but for that specific case, I think it probably isn’t worth proving, because a database lives outside of your application, and it’s the database’s responsibility to manage that kind of data integrity, not your application logic. That’s one of the kinds of “execution-phase failure modes” that I describe in this paragraph of the blog post:

> Parsing avoids this problem by stratifying the program into two phases—parsing and execution—where failure due to invalid input can only happen in the first phase. The set of remaining failure modes during execution is minimal by comparison, and they can be handled with the tender care they require.

[1]: https://news.ycombinator.com/item?id=21478427

See my other comment about this question here: https://news.ycombinator.com/item?id=21478427

> Still no static types for "Strings that end with a dot" or "Strings that match [a-z]+"

Sure there are. :) Technically speaking, anyway. Here’s a type for “strings that end with a dot”:

  -- | A string that ends in the character '.',
  -- represented as a string without its trailing dot.
  newtype StringEndingInDot = StringEndingInDot String

  fromString :: String -> Maybe StringEndingInDot
  fromString str = case reverse str of
    '.':cs -> Just $ StringEndingInDot (reverse cs)
    _      -> Nothing

  toString :: StringEndingInDot -> String
  toString (StringEndingInDot str) = str ++ "."

And here’s a type for “strings that match [a-z]+”:

  data Letter = A | B | C | D | ... | X | Y | Z
  type StringAZ = NonEmpty Letter

Now, admittedly, I would never use either of these types in real code, which is probably your actual point. :) But that’s a situation where there is a pragmatic “escape hatch” of sorts, since you can create an abstract datatype to represent these sorts of things in the type system without having to genuinely prove them:

  module StringEndingInDot(StringEndingInDot, fromString, toString) where
    newtype StringEndingInDot = StringEndingInDot { toString :: String }

    fromString :: String -> Maybe StringEndingInDot
    fromString str = case reverse str of
      '.':_ -> Just $ StringEndingInDot str
      _     -> Nothing

You may rightly complain that’s a lot of boilerplate just to represent this one property, and it doesn’t compose. That’s where the “Ghosts of Departed Proofs” paper (https://kataskeue.com/gdp.pdf) cited in the conclusion can come in. It provides a technique like the above that’s a little more advanced, but brings back composition.

What you’re describe is in a similar vein to what is described in my blog post, and it’s often absolutely a good idea, but it isn’t quite the same as what the post is about. Something like NameType attaches a semantic label to the data, but it doesn’t actually make any illegal states representable… since there really aren’t any illegal states when it comes to names. (See, for example, https://www.kalzumeus.com/2010/06/17/falsehoods-programmers-... .)

In other situations, the approach of using an abstract datatype like this can actually rule out some invalid states, and I allude to that in the penultimate section of the blog post where I talk about using abstract types to “fake” parsers from validation functions. However, even that is still different from the technique focused on in most of the post. To illustrate why, consider an encoding of the NonEmpty type from the blog post in Java using an abstract type:

  public class NonEmpty<T> {
    public final ImmutableList<T> list;

    private NonEmpty(ImmutableList<T> list) {
      this.list = list;
    }

    public static <T> Optional<NonEmpty<T>> fromList(List<T> list) {
      return list.isEmpty()
        ? Optional.none()
        : Optional.of(new NonEmpty<>(ImmutableList.copyOf(list)));
    }

    public T head() {
      return list.get(0);
    }
  }

In this example, since the constructor is private, a NonEmpty<T> can only be created via the static fromList method. This certainly reduces the surface area for failure, but it doesn’t technically make illegal states unrepresentable, since a mistake in the implementation of the NonEmpty class itself could theoretically lead to its list field containing an empty list.

In contrast, the NonEmpty type described in the blog post is “correct by construction”—it genuinely makes the illegal state impossible. A translation of that type into Java syntax would look like this:

  public class NonEmpty<T> {
    public final T head;
    public final ImmutableList<T> tail;

    public NonEmpty(T head, ImmutableList<T> tail) {
      this.head = head;
      this.tail = tail;
    }

    public static <T> Optional<NonEmpty<T>> fromList(List<T> list) {
      return list.isEmpty()
        ? Optional.none()
        : Optional.of(new NonEmpty<>(list.get(0), ImmutableList.copyOf(list.subList(1, list.size()))));
    }
  }

This is a little less compelling than the Haskell version simply because of Java’s pervasive nullability and the fact that List is not an inductive type in Java so you don’t get the exhaustiveness checking, but the basic ideas are still the same. Because NonEmpty<T> is correct by construction, it doesn’t need to be an abstract type—its constructor is public—in order to enforce correctness.

It isn’t broken in lts-10.5, it just isn’t in lts-10 at all. Go to https://www.stackage.org/lts-10.5 and search for ghc-mod—it just isn’t currently available.

Unfortunately, the reason for this is that ghc-mod still isn’t updated for GHC 8.2. It’s almost there—a package candidate has been uploaded that works alright—but it hasn’t made it into the LTS yet. There’s a way to build and install the package candidate in a way that will work with stack, which I have done on my personal machine, but honestly I decided it was just too much for this (already overly long) blog post.

Yeah, I'm quite willing to admit that point-free style seems to often be more harmful than helpful. The comments on r/haskell also pointed out ($) as an operator of possible over-use, which I think makes sense. I just don't want to abuse parentheses, since, coming from a Lisp background, that probably wouldn't be too difficult. :P

This conversation got really out of hand really quickly, so I've stayed out of it, but is Alexis really male-preferred? That's an honest question; I don't know. Wolfram Alpha seems to find the opposite.

http://www.wolframalpha.com/input/?i=Alexis

http://www.wolframalpha.com/input/?i=Alexis&a=*C.Alexis-_*Gi...

Eh, you're right, that came off as far too aggressive—I didn't really mean it to be. Of course the OP isn't going to be omnipotent, but then why default to male? I know English doesn't have singular gender-neutral pronouns, but I think "they" is acceptable now.

And no, obviously I'm not saying people in the field of CS are all misogynist bigots. I'm just saying it's really, really male-dominated, so defaulting to "he" doesn't really cause problems. I'm not trying to attack anyone (and I agree it came off that way, I'm sorry), I just get frustrated when it's a perpetual thing I run into, y'know? Eventually I can get a little terse.

You're going to spend all that work using "the author" everywhere and still manage to get my gender wrong ("his")? Okay. I don't really expect any different in this field, but just noting that.

Anyway, I'm well-aware of the temptation of writing point-free code. I did include the sentence "I can see the road to hell is paved with point-free style" myself, after all. I wouldn't prefer point-free style if it ends up looking indiscernible, but in this case I sort of wanted a way to express semi-declaratively "this function is the difference between these other two functions". Does the version I ended up with do that? Yes. But for all I knew there could have been a much better, more idiomatic way.

But yes, that was both a quest to improve that code and a mere learning exercise. I'm satisfied with the version I ended up with, though I don't think it's perfect, either.

Yep, I posted this on r/haskell and someone pointed this out, which is cool. The provided type for Peg didn't derive Enum or Bounded, but it's a good trick to know.

Ah, no, I probably wouldn't do it any simpler in Racket. Racket tends to de-emphasize more complicated function composition, which tends to serve it just fine. I've always adopted a somewhat pro-functional approach in my usage of the language, but even here there wouldn't really be a distinctly better way to do it.

I guess I was just hoping that Haskell, being a more composition-oriented language in many ways, would have some nice built-in to do that for me.

Yep, that was the inspiration for this. :) I actually linked to it in the short intro bit at the beginning.

I'm curious what conclusions you'd say those are... and if they're good or bad conclusions?

That said, I'm sure I'm totally influenced by various languages I've tried in the past. And FWIW, Racket was also plenty far from my first experience with functional programming. I know so many programming languages that I've gotten pretty used to being able to just "pick them up" in a couple of days (Racket pretty much included).

Haskell... not so much.