Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Haskell in the Large [pdf]

code.haskell.org

Post reply on HN
Print view View original

101–110 of 139 posts

Re: Haskell in the Large [pdf]

#101

Post by stonemetal »

taeric wrote: post #2

"Your choice of programming language can have a real effect on these results over time." Probably more accurate to say "Choice of programming team can have a real effect on these results over time." I want to like Haskell. However, I have given up on wanting to dislike Java. To the point that it is painful to read such things as "you can write Java in any language."

I read that rather differently. I see it as a poke at management that wants to make the move because of hype not a real understanding of what it will take, and not put the effort in training\hiring devs who have as he puts it "have taste and guidance".

Re: Haskell in the Large [pdf]

#102

Post by tel »

dllthomas wrote: post #98
tel wrote: post #75

Earlier quoted context omitted.

Just imagine that every static constraint you want to encode has to be written in the language of the types, a subset of your chosen language. C's language of types is incredibly primitive. Haskell's is quite nice. Agda/Idris/Coq's type language is technically equivalent to its value language so you can encode incredible things. It turns out that due to people's general desire for compilation to always terminate that…

Two asides, which I don't think you missed but I just wanted to expand on... First, "Turing complete" means that you can compute anything anyone else can compute. It doesn't necessarily mean you can do it with a reasonable encoding, or do with it what you need to do with it. At the boundary between systems, encoding matters quite a lot! Second, it's certainly true that there are constraints you can express in Haskell…

I bring up the lack of turing completeness because in the space of type languages you can make even more powerful arguments. What you mention about reasonable encodings is sufficient, but we can get more strength.

And, yeah... even a type system as primitive as C can catch interesting invariants. This is an important counterpoint to the general idea that "types never say anything interesting".

Re: Haskell in the Large [pdf]

#103

Post by marcosdumay »

marmaduke wrote: post #83
tel wrote: post #75

Earlier quoted context omitted.

Just imagine that every static constraint you want to encode has to be written in the language of the types, a subset of your chosen language. C's language of types is incredibly primitive. Haskell's is quite nice. Agda/Idris/Coq's type language is technically equivalent to its value language so you can encode incredible things. It turns out that due to people's general desire for compilation to always terminate that…

Would you then accept a worthless value language if the type language was perfect? Anyway, this was quite an enlightening comment for me: Agda/Idris/Coq's type language is technically equivalent to its value language . Given a sufficiently interesting type language, could we statically type the problem I posed in another comment here https://news.ycombinator.com/item?id=8966065 ?

That depends. Can I get the results directly from the compiler, or must I run the actual program?

About your example, it's not idiomatic Haskell. If you try to code the same exact algithm in Haskell, you'll have the same exact problem (ghc has a warning for it); if you recode it in fmap or list pattern matching that are idiomatic to Haskell, you'll avoid the problem.

Re: Haskell in the Large [pdf]

#104

Post by AnimalMuppet »

tel wrote: post #75
marmaduke wrote: post #65

Earlier quoted context omitted.

So if I understand correctly, the real point is instead of programming defensively at runtime, you can do it in the type system. My main question is the extent to which this is possible in more conventional languages.

Just imagine that every static constraint you want to encode has to be written in the language of the types, a subset of your chosen language. C's language of types is incredibly primitive. Haskell's is quite nice. Agda/Idris/Coq's type language is technically equivalent to its value language so you can encode incredible things. It turns out that due to people's general desire for compilation to always terminate that…

"It turns out that due to people's general desire for compilation to always terminate that the type language behaves quite different from the value language. It also turns out that the type language operates differently because we're more interested in logical constraints than actual evaluation."

If I understand you correctly, if the type system behaves the same as the value system, then it is possible for the compilation to never terminate. Do I have that right?

Re: Haskell in the Large [pdf]

#105

Post by nilved »

the_af wrote: post #87
nilved wrote: post #78

Earlier quoted context omitted.

map fn (head:tail) = (fn head):(map fn tail) map _ [] = []

Your version, while not very different, is not easier to read than that of the parent post. A few weeks into learning Haskell, reading x:xs will become second nature, so much so that "head" and "tail" become noise. (Also, "head" and "tail" are function names in the Prelude, but I'll assume you meant to write "hd" and "tl" or something like that).

    (Also, "head" and "tail" are function names in the Prelude, but I'll assume you meant to write "hd" and "tl" or something like that).
No, I overlooked that. Writing "hd" and "tl" would be opposite to my point! I think that "head:tail" is much more readable and much more informative than "x:xs".

Re: Haskell in the Large [pdf]

#106

Post by Jweb_Guru »

jerf wrote: post #97
marmaduke wrote: post #65

Earlier quoted context omitted.

So if I understand correctly, the real point is instead of programming defensively at runtime, you can do it in the type system. My main question is the extent to which this is possible in more conventional languages.

"My main question is the extent to which this is possible in more conventional languages." It is substantially possible in more conventional languages, however the conventional languages have holes in them which can not be filled in by libraries. For instance, a bog-standard approach in any OO language is to hide the raw constructor and give only mediated access via some other class method (or local equivalent constr…

For what it's worth, the more I have used Rust, the more I have started to think it really is control of mutation ("effective referential transparency") that is important. But given how restrictive Rust is compared to an immutable garbage collected language like Haskell, I'm not sure that will end up being more than an academic question unless you can't afford GC. That is, I think it's easier to just do "immutable by default" but not have to worry about aliasing or lifetimes, than it is to strictly control aliasing.

Re: Haskell in the Large [pdf]

#107

Post by tel »

AnimalMuppet wrote: post #104
tel wrote: post #75

Earlier quoted context omitted.

Just imagine that every static constraint you want to encode has to be written in the language of the types, a subset of your chosen language. C's language of types is incredibly primitive. Haskell's is quite nice. Agda/Idris/Coq's type language is technically equivalent to its value language so you can encode incredible things. It turns out that due to people's general desire for compilation to always terminate that…

"It turns out that due to people's general desire for compilation to always terminate that the type language behaves quite different from the value language. It also turns out that the type language operates differently because we're more interested in logical constraints than actual evaluation." If I understand you correctly, if the type system behaves the same as the value system, then it is possible for the compil…

It's possible, but typically what instead happens is that people sacrifice Turing Completeness in the value language. It turns out that this isn't so painful (strong types help a lot) and then you have guaranteed termination all around!

Re: Haskell in the Large [pdf]

#108

Post by sea6ear »

michaelochurch wrote: post #22
melling wrote: post #8

Has anyone used both Haskell and OCaml (or F#?)? How do they compare in practice? I've been wanting to put some time into a functional language and I've been debating between Haskell and OCaml. Because of F#, OCaml seems like it might be the more practical language (i.e. direct job opportunities). However, excluding F#, Haskell does seem to much more popular than OCaml.

I tend to think of OCaml as a functional C. It's strict and not purely functional. You can write for-loops and while-loops if you want (but you shouldn't) and use refs to have mutable state (but you shouldn't). It has a better module system than Haskell, but doesn't have type classes. It has functors, which are equivalent-- OCaml's functor is an operation over modules and only very loosely connected (through type the…

This book actually teaches C in relationship to previous assumed knowledge of Standard ML (not quite OCaml, but close).

http://eprints.eemcs.utwente.nl/1077/02/book.pdf

I'm not sure I agree with all of the conventions, but it's interesting to see a deliberately functional approach applied to C code.

Re: Haskell in the Large [pdf]

#109

Post by lomnakkus »

tel wrote: post #76
lomnakkus wrote: post #46

Earlier quoted context omitted.

That's only true in the most trivial Turing Tarpit sense, though. Ease of use and defaults matter in practice. E.g. you can do compile-time exhaustiveness-checked pattern matching using the visitor pattern in Java/C++, but try doing that in practice and the amount of boilerplate just becomes unbearable -- and actually obscures (rather than illuminate) the essence of the data structure. There's also the lack of higher…

Additionally, the Turing Tarpit doesn't apply in the level of the type language. These languages actually differ significantly in power since they're not Turing complete. Thus, there are certainly non-trivial and interesting static invariants which you can encode in Haskell and cannot in Java. The most critical and strong common one is probably parametricity.

Oh, certainly. I was just alluding to the futility of the comparison :).

Interestingly[1], the power of the type system seems to conflict somewhat with type inference. Or, at least, that a Turing Complete type-level language like in Shen or Idris does require you to spell out increasing amounts of type information. Obviously, this has to do with undecidability of TC languages, but I kind of think it's interesting that e.g. Haskell seems to occupy a kind of "sweet spot" in terms of inference and being able to tell the programmer when it needs a type ascription. AFAICT that would be impossible in a language whose type system is a-priory undecidable, correct? (Just to spell it out: In Haskell, the compiler knows that if you want feature X, Y and Z, then constructs A, B and C become undecidable... and can tell you so.)

[1] Well, I found it interesting, but I'm a layman at best.

Re: Haskell in the Large [pdf]

#110

Post by tel »

lomnakkus wrote: post #109
tel wrote: post #76

Earlier quoted context omitted.

Additionally, the Turing Tarpit doesn't apply in the level of the type language. These languages actually differ significantly in power since they're not Turing complete. Thus, there are certainly non-trivial and interesting static invariants which you can encode in Haskell and cannot in Java. The most critical and strong common one is probably parametricity.

Oh, certainly. I was just alluding to the futility of the comparison :). Interestingly[1], the power of the type system seems to conflict somewhat with type inference. Or, at least, that a Turing Complete type-level language like in Shen or Idris does require you to spell out increasing amounts of type information. Obviously, this has to do with undecidability of TC languages, but I kind of think it's interesting tha…

Absolutely! The more information a type system can express the less likely it is to guess correctly at what you want just based on your value-level representation of intent.

Which is really fascinating when you think about it. It basically expresses (what we all know) that your code captures only a fragment of the intent of your efforts. Good types can capture much more intent.

So to that end, people explore interactive development. In this scenario, you provide a (potentially partial) type corresponding to the programmatic intent you desire and the compiler conducts proof search to find programs which satisfy that type!

The types are actually more informative than the programs and it provides some evidence that we'd really rather be writing at higher-level typed languages and letting the implementations fall out naturally rather than writing the implementations and hoping that inference can build the proper types.

Or something like that.

Post reply on HN