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

111–120 of 139 posts

Re: Haskell in the Large [pdf]

#111

Post by kyllo »

taeric wrote: post #18
the_af wrote: post #3

Earlier quoted context omitted.

To be fair, that's one sentence in the second to last slide of 42 slides. The presentation, at least what I can see in the slides, is hardly Java bashing :) There are 3 mentions of Java in the whole presentation, only one of which has negative connotations: the one you quoted.

Yeah, the Java bashing I could (and, admittedly, should) have ignored. It is more the crediting the language for the success that I would rather focus on. It is a fairly strong assertion at the end, that I feel needs more support. Back when fewer teams were writing Java applications, I feel similar advantages were felt for it. Of course, I still pine for lisp, so I can not claim to have no biases. (Well, that and MMI…

The entire Java community pines for lisp, whether they know it or not. That's why Apache Ant was invented, it's Java's manifestation of Greenspun's Tenth Rule.

Re: Haskell in the Large [pdf]

#112

Post by thinkpad20 »

tel wrote: post #13
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.

Either one is great. Short of it is that OCaml and Haskell will both teach you a lot of the same things. OCaml has better modularity features (namely, genuine modules which are replicated almost nowhere else) and Haskell has better purity features (namely... purity). It turns out that sophisticated functional programming essentially stresses that good modularity and good purity are both killer features and techniques…

> Personally, I find strict purity more important than expressive modularity. But if anyone could really put them together in a way that worked it'd be great. I'm not so sure such a language exists today, though.

There is Ur, which has both ML-style modules and Haskell-style type classes. It's also pure and strict. And it has advanced type-level programming features and record types. There's a lot to like.

There are a few problems with it, though. It's mostly a one-man project. The compiler is immense, complex and almost entirely devoid of documentation (it's pretty amazing actually, like 1 comment per 1000 lines or so), so contributing is hard. It's very difficult, if not impossible, to use the language for anything but web development: there's no way that I know to execute a program directly, rather than as a sub-program of the ur/web framework. The standard library is tiny and doesn't even include `print`. But even with those warts it has enough good things about it that it's worth checking out.

Re: Haskell in the Large [pdf]

#113

Post by lomnakkus »

tel wrote: post #110
lomnakkus wrote: post #109

Earlier quoted context omitted.

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 interac…

Yes, I've found some of the published Idris videos quite instructive in this regard. Sometimes it can even infer the program fragment that you were supposed to write (given unification and uniqueness constraints), but it seems limited only to demo-level code and frankly at this point I'd be wondering if I got the types wrong and let the compiler infer bad code! (As opposed to getting the program wrong!)

Programming is weird.

Re: Haskell in the Large [pdf]

#114

Post by tel »

lomnakkus wrote: post #113
tel wrote: post #110

Earlier quoted context omitted.

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 interac…

Yes, I've found some of the published Idris videos quite instructive in this regard. Sometimes it can even infer the program fragment that you were supposed to write (given unification and uniqueness constraints), but it seems limited only to demo-level code and frankly at this point I'd be wondering if I got the types wrong and let the compiler infer bad code! (As opposed to getting the program wrong!) Programming i…

Agda's emacs-mode is probably the most developed form of this available today, although Coq's tactics are doing roughly the same thing.

Types can't be wrong in the same way that values can be. Rather, to be more specific, in any circumstance where program derivation could even remotely succeed you will have had to have been specific enough with your types that they cannot easily produce the wrong code. It simply would fail to typecheck---at least eventually.

I wouldn't say that program derivation is limited to demo-level code, I would just say that you cannot expect proof search to achieve large fragments of code. It's just too large of a space!

Instead, it's better to think of it as an interactive game. You describe types as best as you can leaving holes where you haven't figured out what you want. The compiler responds telling you information and guesses about those holes. Furthermore, if you can nail down what you must prove sufficiently well to have confidence that it's the right thing then the compiler can probably do the trivial final details for you.

If you look through Conor McBride's (admittedly vast) literature then you'll find many things discussing this idea with respect to his (now defunct) experimental dependently typed language called Epigram.

Re: Haskell in the Large [pdf]

#115

Post by tel »

thinkpad20 wrote: post #112
tel wrote: post #13

Earlier quoted context omitted.

Either one is great. Short of it is that OCaml and Haskell will both teach you a lot of the same things. OCaml has better modularity features (namely, genuine modules which are replicated almost nowhere else) and Haskell has better purity features (namely... purity). It turns out that sophisticated functional programming essentially stresses that good modularity and good purity are both killer features and techniques…

> Personally, I find strict purity more important than expressive modularity. But if anyone could really put them together in a way that worked it'd be great. I'm not so sure such a language exists today, though. There is Ur, which has both ML-style modules and Haskell-style type classes. It's also pure and strict. And it has advanced type-level programming features and record types. There's a lot to like. There are…

Oh! I've used Ur a bit and spoken to Adam about it briefly. He gave a talk on Ur at Haskell Boston. I wasn't actually aware that it had typeclasses (though it surely has modules).

Honestly, Ur is completely ingenious but there remains an enormous challenge getting it away from being entirely Adam's project. It's completely web-only right now (although Ur is supposedly a more generalized language) as the only compiler is Ur/Web.

Re: Haskell in the Large [pdf]

#116

Post by tel »

the_af wrote: post #89
jlarocco wrote: post #14

Earlier quoted context omitted.

I don't know, but in my limited experience, lazy evaluation makes memory use worse (usually not much), but more importantly makes performance (time and memory) harder to reason about, because you don't easily know when something will actually evaluate. Besides that, there's also not much practical gain from it, IMO. One commonly cited benefit is a function that doesn't use all of it's arguments, therefore saving comp…

> But realistically, an unused parameter should probably be removed. Think about the function if-then-else , which you may be familiar with from your favorite language :) if-then-else true branch1 branch2 = branch1 if-then-else false branch1 branch2 = branch2 Obviously you don't want both branches evaluated in any given invocation, and obviously you cannot remove the unused parameter. Note that the purpose is not to…

Of course, in OCaml that's just

    if_then_else c t e = 
      match c with
      | true  -> t ()
      | false -> e ()
So the question sort of becomes one of how painful thunking or anonymous function syntax is.

Re: Haskell in the Large [pdf]

#117

Post by taeric »

kyllo wrote: post #111
taeric wrote: post #18

Earlier quoted context omitted.

Yeah, the Java bashing I could (and, admittedly, should) have ignored. It is more the crediting the language for the success that I would rather focus on. It is a fairly strong assertion at the end, that I feel needs more support. Back when fewer teams were writing Java applications, I feel similar advantages were felt for it. Of course, I still pine for lisp, so I can not claim to have no biases. (Well, that and MMI…

The entire Java community pines for lisp, whether they know it or not. That's why Apache Ant was invented, it's Java's manifestation of Greenspun's Tenth Rule.

Is it confined to the Java community? Seems a bit more widespread, honestly.

Re: Haskell in the Large [pdf]

#118

Post by lomnakkus »

tel wrote: post #114
lomnakkus wrote: post #113

Earlier quoted context omitted.

Yes, I've found some of the published Idris videos quite instructive in this regard. Sometimes it can even infer the program fragment that you were supposed to write (given unification and uniqueness constraints), but it seems limited only to demo-level code and frankly at this point I'd be wondering if I got the types wrong and let the compiler infer bad code! (As opposed to getting the program wrong!) Programming i…

Agda's emacs-mode is probably the most developed form of this available today, although Coq's tactics are doing roughly the same thing. Types can't be wrong in the same way that values can be. Rather, to be more specific, in any circumstance where program derivation could even remotely succeed you will have had to have been specific enough with your types that they cannot easily produce the wrong code. It simply woul…

I really like this analogy to interactive games, thanks!

I kind of see, logically, that the types can't be wrong in quite as many ways as the code/values/terms, but that's still a (possibly) infinite amount of wrong to contend with! Yes, we can, and frequently do, narrow it down, but still... :)

I've been aware of Mr. McBride's literature for some time, but I haven't ventured in beyond a cursory look at that ridiculously-well-punned Sinatra one. ("Do be do"... something?). It's a bit beyond what I can manage, in theory terms, at the moment.

EDIT: Sorry to sound like an excited puppy, but I don't think the time/place was quite right for me to have gone into or explored this field as I would have liked to as an undergraduate.

Re: Haskell in the Large [pdf]

#119

Post by thinkpad20 »

tel wrote: post #115
thinkpad20 wrote: post #112

Earlier quoted context omitted.

> Personally, I find strict purity more important than expressive modularity. But if anyone could really put them together in a way that worked it'd be great. I'm not so sure such a language exists today, though. There is Ur, which has both ML-style modules and Haskell-style type classes. It's also pure and strict. And it has advanced type-level programming features and record types. There's a lot to like. There are…

Oh! I've used Ur a bit and spoken to Adam about it briefly. He gave a talk on Ur at Haskell Boston. I wasn't actually aware that it had typeclasses (though it surely has modules). Honestly, Ur is completely ingenious but there remains an enormous challenge getting it away from being entirely Adam's project. It's completely web-only right now (although Ur is supposedly a more generalized language) as the only compiler…

Yeah, it has type classes, although the syntax is a little different than how Haskell does it.

Agreed to all of that. I've tried to get into it several times, but I have almost no interest in web development. I'd really like to use it just as a language. It seems like it should be possible to decouple it, but it seems like the only way that will happen is if Adam gets more people in on it. And that's not likely to happen with the scanty documentation and completely impenetrable compiler code. :(

Re: Haskell in the Large [pdf]

#120

Post by thinkpad20 »

tel wrote: post #115
thinkpad20 wrote: post #112

Earlier quoted context omitted.

> Personally, I find strict purity more important than expressive modularity. But if anyone could really put them together in a way that worked it'd be great. I'm not so sure such a language exists today, though. There is Ur, which has both ML-style modules and Haskell-style type classes. It's also pure and strict. And it has advanced type-level programming features and record types. There's a lot to like. There are…

Oh! I've used Ur a bit and spoken to Adam about it briefly. He gave a talk on Ur at Haskell Boston. I wasn't actually aware that it had typeclasses (though it surely has modules). Honestly, Ur is completely ingenious but there remains an enormous challenge getting it away from being entirely Adam's project. It's completely web-only right now (although Ur is supposedly a more generalized language) as the only compiler…

By the way, Adam is apparently going to be a lecturer at OPLSS this summer. That kind of event seems right up your alley; have you ever gone? Any plans to go this summer? I'm hoping to attend.
Post reply on HN