7 ms·

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

by laureny 12y ago

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.

tel 12y ago
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 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.
- dllthomas 12y ago
  The first place which phrase shows up?
  - tel 12y ago
    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".
- laureny 12y ago
  > 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 12y ago
    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 12y ago
      > law-abiding implementations Are you referring to category laws?
      - dllthomas 12y ago
        Lots of typeclasses have associated "laws" that well-behaved instances are expected to abide by.
        laureny 12y ago
        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 12y ago
        I don't think anyone believes that types are sufficient outside, at least outside of a dependently typed language (at which point you'll have more diversity of opinion).
        tel 12y ago
        Types in Haskell won't buy you 100% of what you need, but they may buy you 50%.
cbeustwatch 12y ago
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 12y ago
  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
dllthomas 12y ago
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...
mcguire 12y ago
"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.)
Lambdanaut 12y ago
I always took that quote as more of a feign-arrogance joke than a truism.
jfischoff 12y ago
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"

by laureny 12y ago

tel 12y ago

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 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.

dllthomas 12y ago
The first place which phrase shows up?
- tel 12y ago
  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".
laureny 12y ago
> 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 12y ago
  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 12y ago
    > law-abiding implementations Are you referring to category laws?
    - dllthomas 12y ago
      Lots of typeclasses have associated "laws" that well-behaved instances are expected to abide by.
      - laureny 12y ago
        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 12y ago
        I don't think anyone believes that types are sufficient outside, at least outside of a dependently typed language (at which point you'll have more diversity of opinion).
        tel 12y ago
        Types in Haskell won't buy you 100% of what you need, but they may buy you 50%.

cbeustwatch 12y ago

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 12y ago
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

dllthomas 12y ago

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...

mcguire 12y ago

"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.)

Lambdanaut 12y ago

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

jfischoff 12y ago

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"