Hacker News Reader

Comment by anonnybonny | Hacker News Reader

There is a persistent myth that "A Haskell program that compiles is correct by definition"

Indeed it is "correct" in the sense that it has a very high likelihood (maybe 90% ?) of doing what the programmer intended (Unlike say C or C++ where the probability drops to about 50% for beginners)

However, that is a poor definition of "correct". While it's true that a lot of huge consequences have occurred due to stupid errors like buffer overflows (unintended bug), there are equally disastrous bugs caused by intent - i.e. the programmer had no idea the code could fail.

The biggest challenge to software development is not the "How can I avoid silly mistakes?" but rather "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that

View on HN

You're building a strawman. I've never heard of that myth, the saying is more like "if a Haskell program compiles, it usually works". And you can say the same thing about a couple of other statically typed, functional programming languages.

---

> "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that

Actually languages can help a lot.

This isn't just about "silly mistakes". Compilers are _theorem provers_. Quite literally there's an equivalence between type theory and mathematical logic. I hope you're not saying that math logic doesn't help in modeling real world semantics.

So yes, via modelling types in an expressive language you can at least have proof that the changes you make are consistent with the world view you had before those changes.

Of course people accustomed to less expressive languages like Java won't believe this until they see it. But you should really look into Haskell to see the difference. And dependent typing brings this to the next level.

Ada with Spark is pretty cool.

I used Ada for a few years back when I was working on satellite programs. It's the closest thing to a "If it compiles, it probably works" language that I've ever seen.

I really wish you could use all of the adacore stuff for free in commercial closed source software and just pay for IDE support and maybe some specific libraries.

The point of the type system is that you can express your intent through an invariant or property at one place (i.e. the "head" function can specify that it should never be used on an empty list) and propagate that outwards so that it's enforced at all times.

This is more effective than trying to remember to always check the head function in every single place you ever try to get the first element of a list.

Yes, you can still write a compiling but wrong program. But it will likely be pretty close to what you actually want it to do, and it's easier to notice the behavior is not what you expected in one place, enforce that behavior via types, and see where you went wrong through compiler errors.

The craziest thing about this is that programmers will often think "well, this tech can't prevent every possible kind of bug, therefore it's useless and we may as well use Python/Ruby/JS/whatever".

Programming usually happens in the context of a business, and the technology used has implications in a cost/benefit analysis.

Being able to express invariants at the type level is cheaper for a business at scale.

Programmers who think types let them express their invariants are often ignorant about the fact that expressing those invariants makes their program a mess, so much that they have to consider possibly mutually incompatible language extensions, or reduce modularity of their program to the point where it becomes a pain to compile and becomes hard to maintain, and might require a complete redesign at some point when a minor functional requirement is added...

If you consider this huge overhead in development cost, maybe time is better spent in less intrusive ways of improving software reliability.

Sure, but it's about striking a balance between the type (specification) and the program (implementation). The myth mentioned is just something people say to beginners in Haskell but no experienced programmer truly believes - reason being again this balance. When you can express so much in your type system that the implementation can be mostly automated, you have shifted the semantic mess to a level above but have not really made any substantial progress. Still, it's undeniable that type systems are perhaps the only kind of formal methods who really made it to the mainstream software developer because they can be useful. What I find frustrating is that no one is really guiding the programmers in finding good patterns for achieving a healthy balance specially for code that needs to be maintained and adjusted to new use cases.

I'm not sure they have become mainstream. Java and the like have Generics, but I think that's about where "mainstream" ends. (And even Generics can be problematic).

I think many programmers are skeptical of advanced type systems because the OPs straw man is what gets advertised at the water cooler. I've seen it myself in professional settings.

My impression is that advanced type systems interest people because they're cool moreso than because they're practical tools for reducing errors.

The kind of discussion I see on this post generally reinforces my impression.

That hasn't been my experience so far, but I'd be interested to read in more concrete terms exactly what level of type-level invariant expression begins to create overly-rigid software.

FWIW, I'm not suggesting moving everything possible into types. I'm suggesting types are better than not having them, just like tests are better than not having them.

A software artifact that has a very specific type usually also needs to be very specific in terms of its required preconditions. Which puts a significant burden on the user of that artifact. And now that user probably requires its own additional preconditions to be able to conform. And so on.

I don't know, maybe there is a good way of structuring the software to avoid this effect (I'm not extremely invested in type systems), but maybe it's just a lot of additional pain on top -- too much perceived pain for people who can barely make their software "seems to work".

I can confirm this 100%. Having worked at an old (19 years) Java code-base full of unnecessary patterns & abstractions. Even with really great refactoring help from the IDEA, making meaningful changes is very very time consuming. I've spent weeks on it. The complexity was creeping in over the years and is almost impossible to get out again. But it has types!!!11!

And if I then look at the actual data transformations behind all this code: It would be a 2 day exercise in Clojure to re-build this from scratch.

Java has probably the most notoriously limited typesystem in actual use. Judging type systems by Java is like judging electric cars by the Sinclair C5. Try an ML-family language sometime.

It will have the same intrinsic problems. It doesn't matter that it is Java.

Nonsense. How can you claim that without having seen or tried it?

but that is not the point of Haskell's type system, since it doesn't even begin to try to reach that goal.

firstly, the most available `head` function crashes on half the constructors.

more fundamentally, just try using any file or network io method. you just won't have a clue how it can fail, because it isn't even documented.

there's many methods where the best you can do is work out what exception is being used to wrap a C errno and read the appropriate Linux man page.

at least C documents it's functions that can return errors, and usually encodes them in the type. in Haskell, it's just, "if you're dumb enough to use IO (and what alternative have you got), anything can crash all the time. deal with it".

Haskell is great right up to that point, but that's a critical point.

(I've tried to find ways to deal with this, but the most people seen to refer too something else when discussing how horrible exceptions are, so I wonder if I'm insane)

You're not insane at all. A substantial proportion of the Haskell community (I feel like it's a majority but it's hard to be sure) have a strong distaste for partial functions (e.g. head) and functions that throw exceptions (i.e. where you can't see from the type signature what the possible failure modes are). I'm afraid that momentum means that the base libraries change slowly, but you're a long way from alone.

I suggest you come to https://www.reddit.com/r/haskell/ if you'd like more discussion about it. We often have threads wishing for partial functions to be removed from base!

You might like the paper “Ghosts of Departed Proofs” which shows a great technique for dealing with preconditions in Haskell.

I'll surely read it, but based on the abstract, it's a design pattern for library writers, not a sanity pattern for library users.

it won't let me know how or if the function you wrote will throw an exception, or what kind of exception it will throw, unless it's documented in the type.

but my objection is that many times, the possibly of failure is only present in my generic, language/api agnostic knowledge that a file might not be readable or a ship might drop an anchor on a cable. having thought about it, I then have to read the source code to understand what exception might get thrown, so I can prevent my program from crashing.

(i would prefer it to continue as best as it can in the case that some api is unavailable, which is obviously a usecase dependent decision)

My general approach to programming is that every language at the moment is bad in serious, fatal ways, and that we are all just experimenting and practicing so that 50 years from now we might have a decent approach. Haskell is horrible in some ways, excellent in others, and this paper seems to offer a promising technique.

> there are equally disastrous bugs caused by intent - i.e. the programmer had no idea the code could fail.

At least some of these sorts of bugs (depending on how you define "fail") are captured even in Haskell today by things like Maybe. In fact, if Haskell was total (like Idris) you wouldn't even be able to write a function that searches a list for an element with this type:

    find :: (a -> Bool) -> [a] -> a

Because there's no way for you to magic an a out of nowhere in the empty list case (whereas laziness lets you use bottom). You could however write a buggy find over known non-empty lists because you could always return one of the known elements, types aren't a panacea.

Dependent types go further and let you guarantee things like "zip only compiles for two lists of exactly the same length" which can be helpful in some circumstances (specifically in Haskell we use things like zip [0..] too often to want to change the function literally called zip, but you could imagine another name, perhaps zipExact as in the Safe library).

I suspect you probably already know this and meant a different kind of failure, such as mathematically invalid (which you could probably encode via a sufficiently powerful type system), or a simple misunderstanding of the requirements (which you—as the misunderstander—obviously can't).

> whereas laziness lets you use bottom

in principle, only if you can prove you don't use the result. there's nothing wrong with not calculating a value that doesn't exist.

I can't have much experience with dependent types, but I don't see how a compiler could ever tell if zip took two lists of the same length. Don't dependent types happen at run-time? It seems like you would have to solve the halting problem for them to work at compile time.

It takes a while to grok but for example constant expressions would have type “List Int 7” but a list value from I/O might have type “List Int n” where n is a natural number that also exists at runtime. Now zip would be “forall a, b, n. List a n -> List b n -> List (a, b) n”. Right away you could do a self-zip with your I/O list because the compiler knows that n == n but if you want to zip two different such lists it gets more interesting.

Now you have n, m, and xs : List Int n, ys : List Char m, and you want to do zip xs ys but m doesn’t “unify” with n so the type is wrong. So you have to do an equality check at runtime which gives you a proof of equality or inequality. In the equal case you have a value of type “n == m” and then you can use a language feature to rewrite the type of xs (or ys) according to this equality.

This was written on a phone kind of hastily but maybe it makes some sense.

I've been learning the dependently typed functional language Idris over the past few weeks. The type-safe zip over Vects (linked lists with a length in the type) is a canonical example of compile-time proof that they must be the same length:

    zip : Vect n a -> Vect n b -> Vect n (a, b)

This type specifies that both Vects must be length n. If they are not equal in length, the code will not compile. In fact, this type is so narrowly specified that Idris can infer the entire implementation of the function from it.

Don't dependent types happen at run-time?

Dependent types in Idris occur at compile time and are erased as part of compilation. At runtime, those Vects do not carry around any length information.

It seems like you would have to solve the halting problem for them to work at compile time.

Idris addresses this by having a totality checker. Every function in Idris is marked as either total (known to halt, barring any bugs in the totality checker) or partial (possibly not halting). Only total functions are allowed in types. For example, the function append:

    append : Vect m a -> Vect n a -> Vect (m + n) a

This type uses addition as a type level function. Since (+) for natural numbers (which m and n are) is proven to be total when Idris compiles the library where it's defined, Idris allows it to be used as a type level function.

So how does the totality checker work? Wouldn't that purport to solve the halting problem? No, the totality checker in Idris isn't magic, it's conservative about what it considers to be total. In order for it to declare a function total, it must identify at least one argument that progresses towards a base case at every step. It can do this even with mutually recursive functions.

In practice, if you write an interactive program in Idris, you can make every function total except for main, which presumably contains an infinite loop that checks for input forever.

> This type specifies that both Vects must be length n. If they are not equal in length, the code will not compile. In fact, this type is so narrowly specified that Idris can infer the entire implementation of the function from it.

It's more accurate to say that Idris can guess an implementation of the function, but it's not the only possible implementation with that type. There's nothing in the type to stop the function from reversing one or both of the lists before the zipping stage, for example. More generally, it could randomize the order of elements in one or both of the supplied lists.

That's true, though it has no reason to do those other things. In general it tries to do the least amount of work possible to accomplish the goal.

It's interactive, though, and it's extremely fun to use. It gives you the feeling that you're solving a puzzle, and like a good puzzle game, it can do the obvious bits for you.

Yes, but the "least amount of work", as far as Idris is concerned, has no necessary relationship to what the programmer intended when they defined the type. It guesses the simplest thing that fits, but that's far from a guarantee of correctness.

It is a serious shortcoming that even when you pay the complexity cost of dependent types, you still can't specify the intent in this case. I mean, the semantics of "zip" can't be specified with a type. You can define a "sorted list" or "ordered list" type, but you cannot enforce maintainance of the natural, arbitrary order of list elements. In this sense dependent types are both too complex to reason about and simultaneously not powerful enough to fully specify the function.

One solution to ensuring that the order is preserved (that I've actually used in production Haskell code where this was a real risk) is to use a heterogeneous list instead of a Vec.

  rzipWith :: (forall a. f a -> g a -> h a) -> Rec f as -> Rec g as -> Rec h as

With this type I don't think you'd be able to rearrange the elements, but you do have to pay the cost of using Const everywhere, as in you can specialize approximately my function as follows (handwavy, won't compile):

  zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
  zipWith f as bs = recToVec (rzipWith f' as' bs') where
    as' = vecToRec (fmap Const as)
    bs' = vecToRec (fmap Const bs)
    f' (Const a) (Const b) = Const (f a b)

  vecToRec :: Vec n (f a) -> Rec f (Replicate n a)
  recToVec :: Rec (Const a) as -> Vec (Length as) a

Rec is defined in Vinyl: https://hackage.haskell.org/package/vinyl-0.11.0/docs/Data-V...

> has no necessary relationship to what the programmer intended when they defined the type

Right, for instance I wouldn't be surprised if "the least amount of work" here amounted to reversing both lists as you zip.

> The biggest challenge to software development is not the "How can I avoid silly mistakes?" but rather "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that

You're completely correct in the first half of that but the languages really can help there. Dependent types can be a lot more expressive and capture finer details of your semantics than what you're probably used to.

I simple example is the `pop` function of a List. In Python, you could put strings in a list element. With Java, you can enforce the type of element that goes in a list. In a language with dependent types, you can ensure at compile-time that `pop` can only be called on a non-empty list and returns a list of `length - 1`.

I'd say the difference between Haskell and C are orders of magnitude, not just a difference between 50% (probably a lot lower) and 90% (which would require you to specify the entire contract, at some point you may end up reimplementing business logic inside the type signature at which point you could have bugs there too and you haven't won that much. You still need to use it right). In dependently types languages, it's not unheard of with type signatures longer than the implementation itself.

There is of course no silver bullet, but expressive type systems can protect you against unintended behavior and significantly reduces the number of unit tests you'd need to write.

BTW, buffer overflows etc are a bit orthogonal to this, as that's related to memory safety, not type safety.

Can a dependently typed list be used in the common case where the length of the list is not known at compile time?

Yes. Just like with generics, you can parametrize them, for example in Idris you have the type `Vect n a`, being a list of type `a` with length `n`. An append function could look like this:

  app : Vect n a -> Vect m a -> Vect (n + m) a
  app Nil       ys = ys
  app (x :: xs) ys = x :: app xs ys

Source: https://www.idris-lang.org/example/

Yes, that’s the whole point of dependent types: types can depend on (runtime) values.

Yep - we can even do this today in Haskell without -XDependentTypes :) using things like singletons

I sometimes phrase it as “yeah, your program is correct because it’s type-checked, but who has checked that your types are correct”?

With dependent types some of the logic will be coded in types, and we would need to check those.

Indeed, that’s why Dan North, Liz Keogh, et al have been banging the requirements capture drum for the last ten/twenty years.

Doesn’t mean it might not be useful.

At least now we are checking that two pieces of saying what we want a program to do match up. It's less likely to get both the implementation and specification (in the form of types) wrong. Whenever the program fails to type-check, it will make you think about both bugs in the type and bugs in the code, even if the latter is more likely.

Types can’t encode the specification fully, or require a lot of work to encode a specification (so most people will skip this work).

The simplest example is very common banking and e-commerce logic which is basically a series of checks in the form:

if <some piece of data retrieved at runtime at that particular moment> is consistent with <multiple other pieces whose number and relevance depends on that data retrieved at runtime from potentially multiple sources>.

That's the same logic as not writing tests because your tests might have bugs in.

> "How do I capture this extremely complicated real world semantics in code?" and languages can't really solve that

This isn't true. It's possible to write a symbolic differentiation system using, primarily, Scala's type system. In an elegant fashion.

Similarly, Julia represents math better than, say python or Java. A vector type should not need to know about inner products of vectors, because the math definition of a vector space does not.

This will have large effects on how easy it is to decompose your code into neat little pieces.

> but rather "How do I capture this extremely complicated real world semantics in code?"

I'm not sure that's even it. It's "I don't really understand the requirements until I try to implement them and therefore my first 6 attempts are hopelessly wrong".

The reason dynamic languages are so popular I think is because they make it so fast to iterate through the first 6 attempts whereas statically typed languages make that 50% slower and that generates a huge feeling of helplessness and frustration that you keep doing all this work to satisfy the compiler and then its thrown away.

Of course one can argue that all these people are stupid and should just understand the requirements in the first place, but it's a separate point: that is reality - people find it hard to understand requirements.

But it is one reason I like more "incremental" languages like Groovy since I can iterate really fast in dynamic mode and then tighten up all the screws afterwards by converting it to statically typed code.

It probably "A Haskell program compiles does not crash if you don't use a specific set of functions".

But it probably could be true for a lot of languages, but for Haskell, the set is much smaller

Dependent type can let you achieve some degree of semantic correctness above that. Either by refined types or proof. But it's not generally applied because there are a lot of things we just couldn't prove yet.

The point is that Haskell allows you to push more business logic to the proposition (type) level. Nobody actually thinks Haskell programs can't include mistakes.

Dependent types aim to address exactly "How do I capture this extremely complicated real world semantics in code?". Except now you have the option to capture some or all of those semantics in types instead of terms.

Probably a tangent but I feel like this is only partly true. DSLs are specifically built to do that for example. The languages can meet us half-way so to speak.

Really good point here:

> How do I capture this extremely complicated real world semantics in code?

This is why I keep using Python after having dabbled in other more interesting languages: the probability of writing correct code for me and the team I support is fairly high.

Yea...my first language that I got really comfortable in was Python (used Matlab, Assembly, C, Basic...etc in college). I've since then dabbled in: C++, Ada, Rust, Nim, D, Haskell, OCaml, F#, C#, Java, Clojure, Scala, Kotlin, Common Lisp, Racket, PicoLisp, Groovy, Powershell, Bash, TCL, Julia, APL, Forth, J, Rebol, VBA...the list goes on. I've only ever gotten shallow in these languages, but have always found something missing (I'm sure others have said the same about Python, but I wanted to add my anecdotal experience).

Out of all of those, I've pretty much stayed with Python as it keeps letting me get my job done with minimal code and maximum readability. I've been almost as efficient in Julia and have gradually picked up Powershell's quirks and find them all good for scripting tasks where you don't create too many pages of code.

Would I migrate with a large codebase? It depends on the industry of course, but if it is common line of business applications I'd be hard pressed to find something else. I was really hoping Kotlin could help here with it's REPL/Scratchpad and being on the JVM, but I didn't end up being too impressed (it might take more time).

I don't want to contribute to a static versus dynamic never ending argument. I guess I will say that Haskell, the JVM, and .NET just seem to have to much ceremony around them. I'm sure it's very powerful, but there is a lot to learn that distracts from just writing code.

Reply on news.ycombinator.com