Parse, don’t type-check

https://neilmadden.blog/2020/11/25/parse-dont-type-check/

by todsacerdoti • 6 years ago

178 139 6 years ago

PaulHoule2• 6 years ago

It's the message you should really take away from meta-programming in LISP is that code is a message that can be read different ways.

That's limited though by practical considerations such as the Turing and Gödel results, how your algorithms scale with problem size, etc.

There is room for a revolution in parsing tools, but it seems almost every attempt falls short. (PEG in Python is the latest, maybe they will expose a general purpose interface to it someday, but by then certain performance concerns will be so baked in that features that expand use-cases for parsing such as automatic unparsing and round-tripping won't materialize)

We are still coding to 1970's style 'callback hell' interfaces from yacc when we should be able to write one grammar and get not just the parser but also a set of semantic structures, for instance if you were parsing Java in Java you'd have objects to represent expressions, operators, etc.

nsajko3• 6 years ago

PEG in Python is the latest, [...]

The popularity of PEG baffles me. I guess it ties in nicely with the wider and older pattern of rejecting good formal language and parsing theory, but PEG seems like an all around bad technology; like, is there even a single benefit to using PEG?

The difference between PEG and the usual grammars is that PEG introduces special meaning to the "choice" grammar operation so as to define away ambiguity. But defining away ambiguity actually just "hides" language constructions that will be ambiguous to users. Although PEG notation may be indistinguishable from those used to define CFGs, PEG sucks as a language specification tool as it is unclear what language a PEG defines (unlike with CFGs). From the perspective of implementation, PEG parsers backtrack, meaning either exponential run-time or additional linear memory requirements.

Also some Jeffrey Kegler quotes:

With PEG, what you see in the extended BNF is not what you get. PEG parsing has been called "precise", apparently based on the idea that PEG parsing is in a certain sense unambiguous. In this case "precise" is taken as synonymous with "unique". That is, PEG parsing is precise in exactly the same sense that Jimmy Hoffa's body is at a precise location. There is (presumably) exactly one such place, but we are hard put to be any more specific about the matter.

and

When you do not know the language your parser is parsing, you of course have the problem that your parser might not parse all the strings in your language. That can be dealt with by fixing the parser to accept the correct input, as you encounter problems.
A second, more serious, problem is often forgotten. Your PEG parser might accept strings that are not in your language. At worst, this creates a security loophole. At best, it leaves with a choice: break compatiblity, or leave the problem unfixed. and
PEG is not unambiguous in any helpful sense of that word. BNF allows you to specify ambiguous grammars, and that feature is tied to its power and flexibility and often useful in itself. PEG will only deliver one of those parses. But without an easy way of knowing which parse, the underlying ambiguity is not addressed -- it is just ignored.

PaulHoule2• 6 years ago

PEG for one thing offers the possibility of composibility.

For a language like Python or Java it shouldn't be much harder to add an "unless(X) {Y}" equivalent to "if(!X) {Y}" than it is in LISP if the compiler was structured in such a way that you could take "Java Compiler A" and specialize it to "Java Compiler B" such that one term was added to the grammar and one AST tree transformation that writes the term.

Exclusive of POM files, import statements and other packing material that should be less than 50 lines of code if we built compilers to be extensible.

The arangodb database has a kind of SELECT statement that returns a list of unordered dictionaries which is frustrating if you want to plot the result in a pandas Dataframe. I wrote something in Python using PEG that would parse an adb query and static analyze it and determine the intended field order when definite.

I am up for any compiler technology that makes it easy to do that even if it means I don't get compilation as fast as Go.

Another issue that matters in error handling. Drools is a great rules engine on paper, but as it is composed with an external Java compiler you can often get into cases where the error messages don't make sense at all and it isn't like the Jena rules engine which is simple enough that I could get quick results looking at it in the debugger. That's a complicated example but I think language users deserve better error handling and compiler authors need better tools to do that.

kd5bjo• 6 years ago

Is there even a single benefit to using PEG?

In a formal sense, there are some non-context-free languages that PEG can recognize ( A^n B^n C^n is the classic example ). It’s an open question whether there are any context-free languages PEG isn’t capable of recognizing.

Fundamentally, PEG is a formalization of the common practice of writing a recursive-descent parser: It defines languages based on an exemplar algorithm that parses them instead of the generative approach taken by BNF, which defines how you can enumerate the legal strings of the language. They’re both as mathematically rigorous as each other, but approach the problem space from opposite sides.

For BNF, ambiguity is a question of whether the generation process is reversible: An ambiguous grammar has multiple paths that produce the same string which means that there’s no way to recover the path used to generate that string.

PEG is “unambiguous” because it’s not based on a generative model at all, so this definition is nonsensical. With PEG, we know, by definition, how any given string will parse but it can be hard to enumerate the strings that will parse in a given way. If PEG has an interesting notion of ambiguity (which it probably does), that’s the place to look for it.

valenterry7• 6 years ago

Lisp is certainly the most powerful/elegant meta-programming language out there.

But there is a nuance here: > code is a message that can be read different ways

Think about it. When you read code directly, then you are now dependent on code. And code can change for many reasons, including language changes and mere syntax changes.

For that reason, I like the approach of describing the required actions in a certain data format and then reading this data format in a different ways, in opposition to read code directly. Both in the same language of course. This also reliefs you from having to represent generic expressions, operators etc. you only need the subset that is relevant for you, which is most likely much more coarse grained.

This is imho the cleaner approach but it comes with the overhead of having to design a "sublanguage" in your language and than interpreting it in your language.

benschulz• 6 years ago

I'm not sure I buy the premise. The point of the original article was that you shouldn't dig a hole for yourself to get out of later. Compiler writers usually go out of their way, digging extra deep holes, to accept a broad range of invalid input. Not because they like complexity---though, as a group they.. I digress---but because it lets them give more valuable user feedback.

alipang• 6 years ago

Yeah, the main coherent point I take out of this is that it makes sense to provide capabilities rather than to check them, i.e. if you have access to a certain API then you're by construction allowed to use it. It seems this is something the author has been working on.

This is then somehow shoehorned into "Parse / Don't typecheck" but it doesn't make much sense honestly.

red2awn• 6 years ago

Yeah I am currently writing a compiler, turns out for useful error messages my parser should accept a superset of my language, then validate it afterwards.

nsajko3• 6 years ago

Maybe you should check out the Menhir parser generator instead.

Some links:

http://gallium.inria.fr/~fpottier/menhir/manual.pdf

https://semantic-domain.blogspot.com/2015/11/error-handling-...

https://baturin.org/blog/declarative-parse-error-reporting-w...

mhh__• 6 years ago

The way the D compiler does it is by parsing until it finds an error, marking the node as "poisoned" then walking back up until it can keep going.

It seems to work although I would include a "fail early" flag just to help with enormous error messages (if you apply the principle to sema as well)

AstralStorm• 6 years ago

And pray tell how do you verify that the parser is actually correct? How strict can you get?

Lax parsers are the bane of every web browser's existence.

Ultimately parsing does not get you to correctness, ensuring properties does, and a type system is the lamest way to do it. There are actual logic solvers/theorem provers that can handle properties and are as powerful as programming languages while also ensuring correctness and most importantly completeness.

Some of them were even available as extensions for Java, though constraint programming is not currently in the mainstream. (Besides a small variant called borrow checking, used in Rust for instance.)

wvenable4• 6 years ago

Lax parsers made the modern web possible. New web pages with image tags, forms, and scripts were possible without breaking that page's parsing in older browsers.

jcelerier• 6 years ago

Lax parsers made the modern web possible.

that's the whole problem indeed

anoncake• 6 years ago

That's like saying sloppy programming makes software development possible. At best, it speeds things up (a temporary benefit) at the cost of quality (causing potentially permanent damage).

KirinDave2• 6 years ago

I think that at this point, folks have realized this is not in fact true. If anything, lax parsers made the evolution of the web more difficult and more subject to corporate cooption.

goto11• 6 years ago

This is not due to lax parsing though. It is due to the convention of how to process undefined tags and attribute:

User agents must treat elements and attributes that they do not understand as semantically neutral; leaving them in the DOM (for DOM processors), and styling them according to CSS (for CSS processors), but not inferring any meaning from them. https://html.spec.whatwg.org/multipage/infrastructure.html#e...

This is unrelated to parsing - for example a XHTML parser will be strict and draconian in its parsing, but still process undefined tags and attributes as above.

klodolph• 6 years ago

And pray tell how do you verify that the parser is actually correct? How strict can you get?

The idea presented in the article is that the data type of the parser output ensures that your invariants are satisfied. It’s not a panacea for solving every possible problem with input validation, it’s more of an alternative technique that gives you much better assurances that some of the invariants you think should be satisfied, are satisfied.

cptskippy• 6 years ago

The point of input validation is to fail early, not to ensure the function executes. Returning an empty list when the input is an invalid list sounds like a really bad idea.

What if the function is deleteWhereNotIn( list param )? That empty list just deleted everything.

KirinDave2• 6 years ago

You should read Alexis King's articles on how this is achieved. One of the most imporant aspects of modern parser combinator libraries is that a very small composable core can be exhaustively tested (importantly: with both hand written and random cases) to provide a reliable kernel for parser combinators.

Given that those cited parsers were built from the ground up to mesh with an effective and expressive type system like Haskell's, this problem was significantly reduced. The downside, of course, is that it became quite opinionated.

There is no magic want to wave, but certainly it's easier to work on a common minimal core of components than work on custom ad hoc validators. Lax parsers are not an inevitable outcome; they're a decision propagated by decades of bad opinions being taken as gospel.

one-punch• 6 years ago

An expressive language should let programmers reason about code, including parsers, for their correctness.

You know it is correct when you see it, and you get more confidence in not making silly mistakes with unit tests. This is a different approach to formal verification using logic solvers or theorem provers.

For an example of parsing with Haskell, see this recent discussion: https://news.ycombinator.com/item?id=25212372

This approach, as hinted in Parse, Don’t Type-Check, is to raise the level of abstraction. The jargons are to create a domain-specific language (DSL) to model the problem, as in language-oriented programming.

With this approach, you understand what the code is trying to do and can change it easily because it reads like pseudo-code. (Pseudo-code is usually a synonym for code at the right level of abstraction.)

bern4444• 6 years ago

I don’t understand the idea here. Isn’t typechecking a means of making impossible states impossible? The article references ideas like non empty arrays or limiting the input from all numbers to just integers between 1 and 5 inclusive.

These are both ideas you can express in a type system (quite trivially in most as well). But instead we should use a function at runtime to parse the input and return an object of this type?

Is this article against static type systems, or against runtime type checks? Or both...

Personally I love having a type system and typescript (what I work with professionally) allows for making impossible states impossible just like many other type systems

morelisp8• 6 years ago

Is this article against static type systems, or against runtime type checks? Or both...

It's not "against" anything. It's pointing out that "make impossible states unrepresentable" is poorly satisfied by most typed languages themselves. The more of the language you lift into the parser (decidable! easily-analyzable memory bounds!), the less you need to worry about types.

As a trivial case consider a language where `5 + ""` would fail typecheck. But why even get so far? Why does your parser accept `lit-term := lit '+' lit` and not `lit-term := [str '+' str] | [ num + num ]`, etc.

firethief3• 6 years ago

Because the parser can't typecheck "ident '+' ident", so why make it vastly more complicated only to overlap with a later pass that is necessary anyway?

contravariant4• 6 years ago

parser (decidable! easily-analyzable memory bounds!),

Hahaha, you wish. Sure there are languages that are simple to parse, but they are that way by construction. Parsing arbitrary grammars is hard to impossible depending on how general your class of grammars is.

masklinn4• 6 years ago

As a trivial case consider a language where `5 + ""` would fail typecheck. But why even get so far? Why does your parser accept `lit-term := lit '+' lit` and not `lit-term := [str '+' str] | [ num + num ]`, etc.

Because it's an unnecessary complication to duplicate a few corners of the typesystem as special cases of the parser?

taeric• 6 years ago

Making impossible things impossible seems off. Type checking, by name, is just checking types. Akin to units checking.

That said, some things may be impossible at a piecemeal, but correct as whole. Easiest is really any system. The parts usually do not stand on their own. A gear without the bike is effectively impossible to use, but still correct, after all.

cylon132• 6 years ago

Making incorrect states impossible to represent is exactly what type systems are about. If you're still thinking in terms of something that's basically checking units, I'd recommend experiencing a more advanced type system like Haskell, at least for a few hundred or thousand lines of code. C or Java are terrible examples of what a type system is capable of.

wvenable4• 6 years ago

Pascal has subrange types -- you can declare a type that is 1..10 for example.

Statically typed languages could be more strict and have more basic typing features. In most languages, it's not even as good as units checking because you can't say numeric type X is incompatible with numeric type Y (e.g. Celsius and Fahrenheit).

catlifeonmars• 6 years ago

While it’s true that a gear without a bike is not very useful, one could also argue that it’s also effectively impossible to misuse from a perspective of cyclist safety.

Anyway the real power of the type system is that it gives you, the designer, the ability to define what is correct and what is not correct by composition. For example, you might define a type, CompleteBicycle, which is used as an argument to a ride() function. In your definition of complete bicycle, you could require a non-null gear property of type Gear. Sure, Gear exists independently in the type system, but you haven’t defined any uses for it, so it (by definition) can’t be used (or misused).

Edit: Grammar

the_af• 6 years ago

Making impossible things impossible seems off. Type checking, by name, is just checking types.

That's the purpose of (static) type checking: to prevent incorrect programs from running. Ideally your types encode your valid programs (with some limitations).

masklinn4• 6 years ago

Making impossible things impossible seems off.

It's the entire purpose of a static type system.

All will fail to provide the necessary tools at one point, and many will fail almost immediately, but types are how you encode what is possible, and typechecking is thus what excludes the impossible.

Akin to units checking.

And dimensional analysis is how you know you fucked up and your formula is nonsensical before you even apply it.

brundolf• 6 years ago

I think there were two main concepts:

1) When implementing a type system, you could have a separate representation for a typechecked AST than for a not-yet-typechecked AST, in the same way that you normally have a separate representation for a parsed AST than for a not-yet-parsed token stream. This would ensure against invalid states within a parser by making the type-checking pass another parsing pass instead of a validation pass.

2) The author then seemed to veer into applying this philosophy to application code. However, the author also seems like they've had a lot of experience with languages where the line between parser and application is blurred, so in that context this isn't such a big leap.

rstarast• 6 years ago

I'd say that the type-checker in e.g. Haskell does already do a bit of the "parsing" here, in that it takes code with some type annotations, and returns (on success) that code with fully resolved types. I.e., type variables will be resolved, missing annotations inferred, etc.

That said, the idea of moving parts of the type-checking to the parsing stage is novel and interesting.

nsajko3• 6 years ago

That said, the idea of moving parts of the type-checking to the parsing stage is novel and interesting.

It's exactly the opposite of novel, from the very beginnings of parsing theory its goal was to separate lexical, syntactic and semantic analysis. The benefits of the separation come as both better run-time performance and less code size and complexity.

crazydoggers7• 6 years ago

I use a parser to check for a non empty list return. It’s called a unit test.

All joking aside, what is the practical difference or benefit here to testing?

crazydoggers7• 6 years ago

No one genuinely has an answer to this?

I get that we’re talking about Haskell here which is compiled. But why wouldn’t we talk about running the code through unit tests.

For example the article talks about given function that requires a number that must be between one and five... and then goes on to specify specific grammar rules.

How is that better than simply typing that up in a test.

And by simply running test suites you eliminate issues with bugs in your parser system.

What am I missing?

ghostwriter• 6 years ago

When you have a non-emptiness property on a type, the compiler can guarantee you that all current and future occurences of values of that type in the system will be interacted consistently with the specified non-empty property. Or in other words, the accent is moved from the limited set of units that you are able (and willing) to test to the invariants that will be held for all occurences of the type at all times, regardless of an unlimited number of units that are willing to use them.

valenterry7• 6 years ago

Very simple.

Say you have a user that inputs a list. And then you have another function somewhere in the code, that takes a list, sorts it and uses the max value to send a notification email.

If it's done your way, then you'll have to add an assertion in that function, such as

    if(input_list.length < 1) explode("Bug! Bug! You can't call me with an empty list")

And you will have to write multiple unit tests _each time_ you call this function from somewhere, to make sure it's not called with an empty list.

If you use a compiler... all of this goes away. The function just expects you to give it a non-empty list and if you don't the code just doesn't compile.

Less code to maintain = win.

The price you pay for this is learning, understanding and using a more advanced typesystem. That's not a small price to pay. Pick your poison.

crazydoggers7• 6 years ago

Your example isn’t even what the articles attempt to suggest, and indeed, it’s not even possible, since there’s no way to ensure that the program passes non empty lists at compile.

For example the grandparent article compares these

  validateNonEmpty :: [a] -> IO ()
  validateNonEmpty (_:_) = pure ()
  validateNonEmpty [] = throwIO $ userError "list cannot be empty"
 
  parseNonEmpty :: [a] -> IO (NonEmpty a)
  parseNonEmpty (x:xs) = pure (x:|xs)
  parseNonEmpty [] = throwIO $ userError "list cannot be empty"

He then states

  “Both of these functions check the same thing, but parseNonEmpty gives the caller access to the information it learned, while validateNonEmpty just throws it away.”

But the caller still needs to deal with the empty type. It’s just moved it up higher in the code. Which makes checking easier. He’s referring to this as “parsing”

  “parseNonEmpty is a perfectly cromulent parser: it parses lists into non-empty lists, signaling failure by terminating the program with an error message”

The parent article however seems to want to take this further, but again, to make use of this as suggested by actually parsing still would require unit tests.

A compiler can’t solve the problem of preventing the class of bug you’re talking about, hence why there always needs to be some code that handles cases like empty files or lists etc.

To understand why check out the halting problem:

https://cs.stackexchange.com/questions/72014/what-cannot-be-...

https://en.m.wikipedia.org/wiki/Halting_problem

firethief3• 6 years ago

The parts of this that are fully-baked aren't about parsing or type-checking.

  - the trivial language given doesn't solve anything
  - dependent-typing is more type-checking, not less
  - preferring internal iteration over indexing is several degrees removed from type-checking issue
  - on E: dynamic typing requires type-checking at runtime
  - DSLs are not at odds with static typing

I like this essay. It's a walk through a space of ideas guided by a what-looks-interesting greedy algorithm, along the lines of an "essais" [1]. But I think it's stretching awfully hard to fit the theme it started out with.

1: http://www.paulgraham.com/essay.html

nmadden4• 6 years ago

Thanks. For what it's worth, the flow of thought was the following:

1. The original "parse, don't validate" essay clearly describes why parsers are preferable to validators.

2. It uses a type system to make illegal states unrepresentable in a programming language - but a type system is a validator under its own terminology.

3. What would a parser-like approach to solving the problem look like?

I believe that actually adjusting the programming language grammar (and thus the actual parser) is clearly a parser approach to solving the problem. Abstraction is also, to me, a parser-like approach to solving the problem - it transforms code that allows illegal states into code that enforces particular invariants. I probably didn't make those connections explicit enough in the blog.

Perhaps the diversion into object-capabilities is a bit off the track, but I found it an interesting connection at least. (And frankly, I'm usually close to the sole audience of my blog so I better make it interesting for me!)

Edit: formatting

contravariant4• 6 years ago

I see, it's an interesting line of thought but I think trying to move type checking into the grammar is fundamentally a bad idea. You don't want to mix grammar and semantics because that's not how people think about code.

That said I agree that it is interesting to see what the 'parse, don't validate' approach to type checking would be, but I think it should still take place on the type level.

And I think this leads you towards interfaces, though perhaps we can improve interfaces by embracing the idea. Taking C# as an example interfaces basically ensure that if the type check succeeds then the function will be given an object that supports the methods of the interface and only the methods of that interface. Even further the methods and fields names of the interface can conflict with the fields and method names of the object but the type checker 'resolves' those conflicts and essentially returns a 'parsed' object with the right methods.

Unfortunately this doesn't yet allow for arbitrary conditions (explicitly). Provability is always going to be an issue so let's say we fix that by dynamic type casts. Then I think the behaviour we want is essentially an interface defined by a function

IMyInterface parse(MyObject: MyType)

where the constructor of IMyInterface enforces some checks and an object implements the interface if it defines an implementation of 'parse'.

Now we only need a language to support this. Maybe we can persuade the Julia guys? They seem to like this kind of type-polymorphism based aproach.

Edit: Just checked, apparently they have implemented it, it's just called 'convert'.

cannabis_sam• 6 years ago

I believe that actually adjusting the programming language grammar (and thus the actual parser) is clearly a parser approach to solving the problem.

How do you get the properties of type safety (progress and preservation) in this case?

alisonkisk• 6 years ago

The author contradicts the headline in the body. This seems like a poorly written bit of highbrow content marketing for his book.

morelisp8• 6 years ago

Rhetorical Flourishes Considered Harmful?

Cu3PO42• 6 years ago

The title suggests that type checking should be replaced with parsing, but that's not the article's message. Rather the article recognizes that powerful type systems (more powerful than in many mainstream languages, perhaps) are a great tool to enforce certain invariants. However, those type systems (dependently typed ones, in particular) are also complex and often fickle beasts. The article suggests that it may therefore be worth replacing them with different, less powerful, but easier to work with approaches.

carapace• 6 years ago

In re: E and capabilities, see also "macaroons":

This paper introduces macaroons: flexible authorization credentials for Cloud services that support decentralized delegation between principals. Macaroons are based on a construction that uses nested, chained MACs (e.g., HMACs) in a manner that is highly efficient, easy to deploy, and widely applicable.
Although macaroons are bearer credentials, like Web cookies, macaroons embed caveats that attenuate and contextually confine when, where, by who, and for what purpose a target service should authorize requests.

https://research.google/pubs/pub41892/

vzaliva• 6 years ago

Is it me misreading it or the author trying to re-invent dependent types?

dgentile• 6 years ago

The problem is that fundamentally we always have types. We must define different types of bytes and the different things we can do with those bytes. If you can generate a binary from your programming language, it must use a form of static or inferred typing to know what assembly code to generate. A dynamic language just checks at runtime, and adds a bunch of overhead, which isn't always necessary, and is more likely to result in weird "defined" behavior like we get from javascript and php. Typescript is very popular because you can make certain guarantees at compile time, instead of a vague hand-wave of "the code looks good".

As an example of the benefits of type-checking, in the Vulkan api, there are a lot of handles. VkRenderPass, VkPipeline, VkSwapchain, VkDevice, etc. All of these are just pointers. If we take a function like:

    void vkDestroyCommandPool(VkDevice,VkCommandPool,const VkAllocationCallbacks*);`

And remove the type checking:

    void vkDestroyCommandPool(void*,void*,const void*);

It is the same API, but without type-checking. Even if the parameters are labelled, with this new API I could mess up and pass the wrong thing.

wool_gather• 6 years ago

The article is not even remotely suggesting removing type information. On the contrary, it's talking about some ways to augment a type checker with different grammar or ways of constructing APIs.

MetaDark• 6 years ago

No, but you can always encode this augmented information in types to make it explicit, and possibly help the compiler make optimizations. Using a weaker type when you can use a stronger type is just as bad as removing type information.

inetknght2• 6 years ago

In C perhaps that's unfortunate. I'm sure glad we have more modern C++ that would enforce pointer types.

... as long as the functions aren't declared in `extern "C" { ... }`

which many libraries are. That's for many reasons, some of which include the very type system itself being an inhibitor of easy integration across languages.

moonchild2• 6 years ago

I don't quite follow. C will also prevent you from mixing up disparate pointer types; and c++ has no protection against void pointers.

cle2• 6 years ago

I think it’s important to be more specific here. You can always mess up and pass the wrong thing, the type system can never know what is semantically correct, no matter how strict your types are. They’re about ergonomically reducing the space of valid programs.

There are a lot of interesting tradeoffs to be made there. Over strict specification (whether parsing or type checking), specifically checking for invariants that aren’t actually useful, can make code and systems brittle and hard to change, just like under specifying them. The specifications can also be different depending on what you’re doing with the data.

Also as the expressiveness of types increases, the space of possible ways to constrain your program space goes up, along with the complexity of the transformations of that space, making it difficult to understand what the valid program space actually is, hard to understand when you’ve accidentally excluded perfectly valid programs, etc.

So yes, fundamentally there are always types and underlying structure to useful data, but saying that it has “a” type is dramatically over-simplifying things.

choeger• 6 years ago

I think it’s important to be more specific here. You can always mess up and pass the wrong thing, the type system can never know what is semantically correct

This is not true. Consider the map function of a typical functional language with parametric polymorphism:

map : (a -> b) -> [a] -> [b]

That signature is complete, it covers everything there is to know about the function. And, except for trivial implementations, there is no way to implement it wrongly.

In some cases, one can even rule out trivial implementations and infer the correct implementations from the type signature alone.

In any case, there is no "semantically wrong" input to such a function. It is just a function and totally agnostic regarding your use case.

valenterry7• 6 years ago

I think it’s important to be more specific here. You can always mess up and pass the wrong thing, the type system can never know what is semantically correct, no matter how strict your types are.

Can you give an example?

mumblemumble2• 6 years ago

I don't see this as challenging anything that the article is ultimately proposing. See, for example, the last paragraph:

I thank the flying spaghetti monster almost every day for the type system in my day job (and that is only Java’s tepid concoction)...

Isn't exactly a statement you'd expect to find in the concluding remarks an essay whose goal is to question the value of type systems or static types. It's presumably something more nuanced like that. Maybe something more like

we are in danger of thinking that type systems are the only way of achieving correctness in software construction.

Which seems reasonable to me. Type systems are excellent for eliminating certain classes of errors. But we shouldn't let them become a golden hammer. Even if they can be used to eliminate other classes of errors, that doesn't necessarily mean they're the best tool for the job. Lately, for example, I've been seeing some disillusionment with dependent typing, and people saying, in effect, "Yeah, it's a really impressive technique, but try to find a simpler solution first."

And some of those simpler solutions do come from the dynamic programming world. For example, "You can then go further and remove the more primitive operations, only allowing access to the higher level abstractions," is another excellent way to make illegal states unrepresentable. And you don't need shiny new programming languages or rocket powered type systems to do it. I was really rather disappointed that that section of the article gave a nod to Dijkstra, but completely failed to mention Alan Kay's The Early History of Smalltalk, which was, to an approximation, several thousand words' worth of grinding away on that point.

moonchild2• 6 years ago

And indeed, in opengl, where all handles have the same type (GLuint), it's very easy to mix up handles of different types.

It's quite easy to fix this without breaking ABI compatibility; but it hasn't been done in any implementation that I know of.

darkr• 6 years ago

https://github.com/fthomas/refined

cryptica• 6 years ago

Reading articles like this makes me want to avoid Haskell.

It seems like the language is so over-complicated that it requires developers to invent an entire religion to be able to effectively apply it to real world use cases.

From the perspective of a non-Haskell coder who worked with many different mainstream languages, I find that many articles written about Haskell, Erlang and Elixir seem to have no meaning outside of their own narrow domain; they try to present some solutions as some universal insight which is applicable to all languages. In fact, they seem to revolve around solving problems which the language itself created and only exist in that language.

I like languages which stay out of my way and don't create any new problems or require inventing unnecessary abstractions and ideology (my OOP philosophy is so simple, I could explain it to a 10 year old). I can't believe that you would need several articles to explain to developers how to do something as trivial as validation. It's not rocket science (...well it shouldn't be). In the communities I participate in, most developers seem to intuitively know how to do validation... There are multiple ways to do it. You just have to think a bit to figure out which way is the best for your project.

A lot of these trendy languages seem to be on a futile mission to try to automate away some of the complexity of building software. Building software is irreducibly complex because there are always going to be a huge number of possibilities at every step; this is because the real world (which software tries to model) is complex, always more complex than it seems. That's why I like simple expressive languages which stay out of my way. Any tool which constrains my thinking into specific narrow patterns is going to make my work harder and more error-prone, not easier.

reuben364• 6 years ago

Reading articles like this make me want to avoid OOP.

It seems that like the concept is so over-complicated that it requires developers to invent an entire religion to be able to effectively apply it to real world use cases...( my procedural philosophy is so simple, I could explain it to a 10 year old).

There are many ways to build software, but only few ways to build it reliably. One major aspect of reliable software is composability, so that may ensure correct large systems are out of correct smaller systems. Correctness in the small, trivial bits and their glue is what makes correctness at large. You say you just have to think about what's best for your project. Why not think about and understand the problem in general and build tools to tackle the specific complexities you have.

Feel free to not use Haskell. Just keep in mind that you too live in a bubble with a certain mixture of doctrine and trade-offs.

lambda_obrien3• 6 years ago

Haskell has been around for a really long time, almost 4 decades. It's used quite a bit by programming language theorists and category theorists to prove their mathematical theorems in a real language. It's not trendy or experimental, although some parts are one or both. There are about 5 ways to do everything in Haskell, but that's not bad once you understand it. It's not a language you can just pickup in a weekend and easily Google questions about, it's generally used for applications that require some higher level of data and quality assurance, from a fully proven program using Coq to simply a program that's easier to use equatorial reasoning on, like industrial processes or stream processing pipelines.

Erlang has been around about as long. It's also not trendy, and it's designed for telecommunications applications, where the extremely distributed actor model is great. Others might try to shoehorn it everywhere, mostly via elixir, but it's a very reasonable language for many uses, like chat programs or distributed in memory stores.

You might want to understand something before you crap all over it, everything exists for a reason, try to figure out the reason.

betaby2• 6 years ago

Your statement about Erlang in telecom is mostly a myth. There was one somewhat successful niche piece of equipment from Ericsson and even that was ~20 years ago. Erlang is basically unheard in the telecom field.

dtwhitney• 6 years ago

Haskell simply makes you do a thing you should do: check that the thing you expect to be there is actually there. You can think of it simply as the compiler acting as a testing framework.

On the other side there are things like TypeScript where selecting the 'n' index of an array does not give you a type representing the fact that the item may not exist, and thus does not force you the check if it does. You may call this "getting out of your way", but I don't see how this makes software less complex - it makes bugs more difficult to track down and necessitates more tests, which could simply be removed by an adjustment in types.

TyoeScript/JavaScript is easier to learn, but dear God does it offer so many ways for your to shoot yourself in then foot.

tome2• 6 years ago

Reading articles like this makes me want to avoid Haskell.

Huh? The article doesn't even mention Haskell!

valenterry7• 6 years ago

I find that many articles written about Haskell, Erlang and Elixir seem to have no meaning outside of their own narrow domain; they try to present some solutions as some universal insight which is applicable to all languages.

As a developer who does not use Haskell (but understands most of it), let me put it into perspective:

If you write an article about the visitor-pattern or any kind of other OOP pattern, how do you think this is perceived by a developer who ever only wrote assembly?

Yes, they will think in the same way you think right now. This phenomenon has been described e.g. here: https://wiki.c2.com/?BlubParadox

Fact is that from the perspective of a Haskell developer, you are writing unorganized spaghetti code when not using the techniques they write about. In the same way you probably would see an assembly developer writing spaghetti code instead of using OOP techniques.

I like languages which stay out of my way

Languages that stay out of _your_ way are languages that encourage the style that _you_ are used to. There are no languages that generally stay _out of the way_ because that's not possible and not even desired. So saying this just means "I want a language where I don't have to learn another way of doing things". That's fair, but it should be emphasized.

my OOP philosophy is so simple, I could explain it to a 10 year old

Many people learn Haskell first and than have trouble learning classical OOP in e.g. Java. And the other way around. What does that tell you?

dragonwriter• 6 years ago

I find that many articles written about Haskell, Erlang and Elixir seem to have no meaning outside of their own narrow domain; they try to present some solutions as some universal insight which is applicable to all languages. In fact, they seem to revolve around solving problems which the language itself created and only exist in that language.

I don't find that to be the case often; Haskell articles, specifically, often have solutions to problems that static typing brings to the fore (they usually exist without it, but are less obvious without static typechecking and the solution approaches are sometimes different) and may present solutions that require a type system more powerful than is typically available outside of Haskell (though they are usually translatable to a weaker type system with some loss of safety.)

In fact, I've learned a lot applicable to programming in languages like Python, Ruby, JavaScript, and C# from learning a bit of (and reading articles focussing on) each of Haskell, Clojure, Erlang, and Elixir. Most paradigms can be applied productively in most languages if you are familiar with the paradigm and target language (though they're are definitely things that depend on being on one side or the other of the static/dynamic divide.) And even workhorse languages these days tend to be multiparadigm to start with, so learning techniques from the languages where a paradigm has been most fully explored and is most naturally expressed is often a good source of understanding to apply in other languages when that paradigm is the right choice.

A lot of these trendy languages seem to be on a futile mission to try to automate away some of the complexity of building software

All languages higher level than raw machine code exist for primarily that purpose (and, for that matter, the design of modern machine instruction sets itself does some of that, too.) That isn't limited to “trendy” languages, which probably just means popular ones that are outside of your particular zone of preference established through familiarity.

didibus6• 6 years ago

Using parsing and abstractions for safety is the basis of why Clojure, even though dynamically typed, is a relatively safe language[1]. The abstractions are safer in Clojure: no for loops, no while loops, only higher level iteration and transformation constructs, data interfaces are all immutable and functional. Shared state can only be used through higher level managed APIs, numbers auto-promote themselves to higher precision, there's no linear search APIs to force the use of indexed data-structures instead, etc.

And for parsing: Spec is a way to define contracts, but it's actually a parser DSL. User defined macros which specify a Spec will have their input parsed by the Spec at read-time, and if the Parser fails, a read error will show up. Unfortunately, this only happens for macro, but the article made me curious about possible value of having this done on functions as well.

An example of this is say you have some macro which would let you do:

(:from coll :take 5)

Your Spec can parse this, and error if the first element isn't :from, the second element isn't a reference or a collection literal, the third element isn't :take, the fourth element isn't a reference or an int, as well as if it isn't called with exactly 4 elements. And all this happens at read time, when the code is parsed. You could go further, and if a collection literal was used, you could assert that the take int isn't bigger then the number of elements in the collection literal.

Now, what I've observed is that reference types kind of limit what the parser can do. I'm not sure the article addresses that. Like in my last example, I can validated the range of take over the size of the collection, but not if the collection is a variable. How do I track those references? Maybe somewhere else in the program you can find the collection literal, but not here.

P.S.: It's hard to know why Clojure demonstrates relative safety, and I assume here it has a little bit to do with the abstractions it uses and this parser Specifying mechanism. But it's also likely it's all due to the REPL or something else.

[1] https://www.i-programmer.info/news/98-languages/11184-which-... - Shows Clojure as having some of the least number of defects per commits

archgoon• 6 years ago

Clojure, for those unfamiliar with the language, unsurprisingly, does in fact allow for both 'for' and 'while' loops, and are part of the core language library.

https://clojuredocs.org/clojure.core/while

https://clojuredocs.org/clojure.core/for

And here are examples picked from a random repository of these constructs being used in the wild:

https://github.com/ring-clojure/ring/search?q=while

What clojure does do is also provide a number of higher level control constructs, and, by the nature of the syntax of the language, puts them on the same level as 'while' and 'for', which themselves are part of a library, rather than baked into the language itself.

This can, of course, be done in other languages, using fluent interfaces.

https://en.wikipedia.org/wiki/Fluent_interface

But is typically much more awkward and harder to compose. Also, you typically have to wrap expressions in lambdas.

didibus6• 6 years ago

Not to be too nit-picky, but it doesn't actually have a for-loop. The for you linked to is not a for-loop but a for-each loop (simply called for). Well it is actually more restricting even then a for-each loop, as it maps over elements and can only return a collection of the same length as it iterates over.

That said, you're correct it does have a pseudo while-loop. Though it will still force you to use a managed mutable container along with it, which is still safer than without. Also, it's a very ackward while-loop, as it doesn't support continue or break, that's because in reality it isn't a real while-loop, it's a fake while-loop built on top of a recursive loop.

And for all other readers, it's true, Clojure doesn't disallow the use of less abstract less safe construct, it simply makes them more ackward to use and not the default and obvious choice. The reason for this is also something the article didn't bring up, but higher level safer abstractions often come with a performance cost. This is why most languages have escape hatches for whatever safety mechanism they provide, and why Rust lang loves to talk about "zero-cost" abstractions.

fulafel• 6 years ago

Sibling thread went into the nature of things in Clojure that are not "true" low level loop constructs, so just to point out, Clojure does also have loop/recur where you have more control on looping.

jldugger• 6 years ago

Isn't the first step of writing a type checker to write a parser?

raiflip• 6 years ago

Types are just labels that a parse has already been done and doesn't need to be done again. Use them when you don't need to parse again, don't when you do want to parse again.

gugagore• 6 years ago

I like the principle of "make unauthorized states unrepresentable", but it makes me nervous, or at least evokes a nuance that is well addressed by https://github.com/tree-sitter/tree-sitter

Robust enough to provide useful results even in the presence of syntax errors

Especially when it comes to human-generated input (but even outside of that) it is beneficial to have a representation for unauthorized states, so long as you can easily detect that that's what you're representing. That allows you to better report errors, or try to mitigate them.

In other words, don't forget to have an https://wiki.c2.com/?EscapeHatch

mumblemumble2• 6 years ago

The dictum is usually phrased as, "make illegal states unrepresentable". Perhaps this is just playing with semantics, but, to me, that difference in wording is incredibly important.

An unauthorized state (which I'm interpreting here to mean an error state) may not be on the happy path, but that doesn't necessarily mean it's invalid. For example, "the user is trying to open a file, but they don't have permission to read it" is a valid state. The resulting error condition is also valid, even if it's not somewhere they want to find themself.

An illegal state is, in the context of this phrase, meant to be one that's nonsensical. Perhaps "invalid" would be a better word. Think negative array indexes in languages that only let you index from the front of the array, or objects that are only halfway initialized. Situations where, having entered such a state, the behavior of the program is now undefined. We should strive to make it physically impossible get the program into a state where its behavior is undefined.

ncmncm• 6 years ago

The author clearly does not understand what type checking is about.

In a good strongly-typed language, types don't just prevent errors. They are put to work to perform computation. They choose overloads, and therefore control flow. Different overloads produce different results, therefore data.

In the extreme, the type organization of a library is itself a program, one that runs at compile time, and generates the program that will then be compiled and run.

EugeneOZ• 6 years ago

It really depends on language.

WalterBright2• 6 years ago

The essential message is to make illegal states unrepresentable.

That's why, in C we have:

    if (a = b)

and:

    if (a < b < c)

that cause (in some compilers) warnings. I wanted to make this an error in D. One option is to check for and disallow them after the parse, but that left:

    if ((a < b) < c)

as still an error. I wanted to allow these constructs to remain if they were parenthesized, as that would imply they were deliberate. (Yes, parenthesized expressions could be a separate grammar, but I thought that was an awful idea.)

The solution is to fix the grammar, so they wouldn't even parse. The beauty of this is one doesn't have to enable warnings, or have a separate check for them, it just won't compile. Even better, D's expression grammar is the same as C's, and it did not upset anything else in the grammar as a side effect.

Based on my experience at Boeing designing hardware, defining the problem out of existence is a great way to design robust systems.

andreareina• 6 years ago

What's your take on desugaring it to

    (a < b) && (b < c)

ala Python?

Speaking hypothetically of course, since it would be a breaking change.

st1ck• 6 years ago

Note that Python applies same logic to other operators, which can be pretty unintuitive:

    1 in [1,2,3] is True

evaluates to False.

WalterBright2• 6 years ago

That was considered, but the problem is what does the user think when he sees `a < b < c` ?

1. is it intended to be the C way?

2. is it the Python way?

3. did the user assume it was (1) or did he assume it was (2) and guess wrong?

This means that such expressions are a never-ending red flag for a code review. Hence it is made an error. The user can still get the C behavior by using parentheses.

Note that if D was a Python-derived language, then selecting (2) semantics would be a no-brainer. But as a C-derived language, it has to be an error.

lispweeniejr• 6 years ago

this is one place where prefix notation really shines:

    (< a b c)

lmm• 6 years ago

I would certainly hope that a type "checker" returns a more detailed representation of a program than a parse tree - one in which all expressions are typed and ill-typed expressions cannot be represented. So the premise is fundamentally wrong.

Are there non-type ways to improve program safety? Maybe. But since we all understand types and types can cover all the cases we've managed to find so far, I'd stick to types unless and until we can demonstrate a need for something else. Yes, handing out fundamentally unsafe APIs like array-access-by-index is a bad idea - but trying to put types on those APIs is the easiest way to see that they're the wrong abstraction. If you insist that your APIs be type-safe, you'll naturally be guided away from APIs like get-at-index and towards APIs like map / fold / find.

nmadden4• 6 years ago

I would certainly hope that a type "checker" returns a more detailed representation of a program than a parse tree - one in which all expressions are typed and ill-typed expressions cannot be represented.

Do you have an example of this? It is not my experience of compiler intermediate representations or ASTs that they have this property.

But since we all understand types and types can cover all the cases we've managed to find so far, I'd stick to types unless and until we can demonstrate a need for something else.

This doesn’t really argue with anything I wrote in the article. (Although I’d argue that nobody strictly “sticks to types” as their sole way to enforce correctness).

trying to put types on those APIs is the easiest way to see that they're the wrong abstraction

I’m not sure I’d say it’s the easiest, but it certainly helps. I love Haskell as a language, primarily because it has a lovely set of well-designed abstractions. It’s clear the design of those abstractions were guided by types and benefit from that. Many of them remain good abstractions when translated to untyped languages.

tome2• 6 years ago

Typed intermediate language. GHC has always used a statically typed intermediate language, one of very few production compilers to do so. (Maybe even the only one.) Let's keep that property. Richard's thesis makes it clear that doing so is not straightforward.

-- Simon PJ (https://github.com/ghc-proposals/ghc-proposals/pull/378#issu...)

So it looks like it's rare to even have a typed intermediate language, let alone one whose structure forces it to be well typed. The latter would require some sort of dependent types.

jayd16• 6 years ago

Isn't this just saying the exact same thing as the original article but with pedantic word games? A type checker includes a parser, a lexer, a syntax tree builder and the type checking itself is the specific grammar the author is looking for. Am I missing something?

Parse, don’t type-check

Related Stories