[laureny]

I'm getting tired of reading:

> This is why we hear that Haskell reprise if it compiles, it works.

If this were true then functions would not need bodies, you would just define their signatures and move on with life.

The truth is that even with its superb type system, Haskell still needs to run your code. Your code might be statically correct but its runtime is up to you.

I would prefer it if people rephrased this claim like "If it compiles in Haskell, it's more likely to run than if it compiles in Java".

More honest.

[dllthomas]

Of course it's not at all true that anything in Haskell that compiles works for any task X. It's not even quite true that, setting out trying to build something that accomplishes X, X will always be accomplished as soon as you get it to compile. However, in my experience, it is frequently true that it is surprisingly the case - I put together something somewhat large and it works first time where in another language (that I might even know better) I'd expect to have a few bugs to fix. People joke around, but I don't think anyone actually makes the either of the stronger assertions and expects to be believed, in which case I don't really think there's a problem (but I'm sorry if it bugs you!) - on the other hand, maybe I'm being overly charitable and people really are intending the stronger forms...

[tel]

Well, as you go to the next steps you can use proof search techniques to do exactly that: write your types and your programs write themselves as the "only possible implementation".

This is already possible sometimes in Haskell so long as we restrict ourselves from pathological values like exceptions and non-termination. In fact, the first place this phrase shows up is Russel O'Connor talking about highly polymorphic lens code.

http://r6.ca/blog/20120708T122219Z.html

This kind of type limitation of possible implementations is called parametricity and is difficult to encounter even in most typed languages as it requires purity.

[laureny]

> write your types and your programs write themselves as the "only possible implementation".

But there are only very few type signatures for which this is true, even if you stick to totality.

[tel]

In practice types often winnow the possible implementations to be a relatively small set. This effect is improved if you also include notions of law-abiding implementations as Haskellers often do. At the end of the day, it's true that implementations (don't yet) write themselves, but, more realistically, that the constraints of type and theory drive you naturally to the correct solutions even if you never once figure out the "operational" aspect.

That occurs quite often.

[ademarre]

> law-abiding implementations

Are you referring to category laws?

[dllthomas]

Lots of typeclasses have associated "laws" that well-behaved instances are expected to abide by.

[laureny]

But these are not enforceable by the type system (at least in Haskell), kind of supporting my point that types alone are rarely sufficient :)

[dllthomas]

The first place which phrase shows up?

[tel]

Mm, I think I went too far there. I was thinking "confession of a Haskell hacker" but got that conflated with "if it types, it's right".

[mcguire]

"If this were true then functions would not need bodies, you would just define their signatures and move on with life."

That's because both addition and multiplication, for example, have the same type signature.

    Prelude> :type (+)
    (+) :: Num a => a -> a -> a
    Prelude> :type (*)
    (*) :: Num a => a -> a -> a

A better rephrasing might well be "If it compiles and you've used the right operations, which is made easier because most of the wrong operations will blow chunks all over the place, it works."

Dependent typing anyone? (I think what you're looking for goes by the name "code extraction" in Coq, but I've never gotten into it as a programming environment.)

[jfischoff]

Yeah its a bullshit line. There are certain class of functions in Haskell that can be completely derived from their signature (see djinn) but Haskell's type is not strong enough for automatic formal verification.

I would prefer is people just said "I program faster in Haskell"

[cbeustwatch]

And you know what I am tired of reading, Cedric Buest?

You trolling every programming language discussion with fake names and sock puppets relating your fake made up experiences with functional programming. Do you have no dignity?

[lectrick]

You know you're not covering your tracks very well when there are full-fledged watch accounts named after you which are trying to keep your uninformed opinion in check lol

[Lambdanaut]

I always took that quote as more of a feign-arrogance joke than a truism.