Live data from Hacker News

Haskell in the Large [pdf]

code.haskell.org

91–100 of 139 posts

Re: Haskell in the Large [pdf]

#91
post #5

Earlier quoted context omitted.

A pretty common idea in Haskell-land is that "the next Haskell would be strict". Laziness was once a dreamy ideal execution strategy, but thanks to Haskell the practical tradeoff is better understood. At the same time (as the slides note) the strict/lazy divide is hardly decided! As many people who would rather Haskell be strict are willing to defend laziness to the death for being the key reason Haskell is so compos…

I tend to feel this is one area where perhaps Scheme had the right idea (if you ignore set!). Now, I don't know a whole lot about Haskell, but one of (IMO) the elegant parts of Scheme is that you can choose when and where to use streams instead of lists. The main benefits of streams vs. lists is usually composability, but also that delayed computation can save you from computing something you'll never need. In this w…

The typical idea is that you almost always want "spine lazy" data structures. So, streams are almost always more valuable than strict lists.

In my mind, I tend to think of this as being true up to the point where the size of the structure is statically known. Thus for fixed-sized vectors (or arrays), spine strictness is very important—it gives you better control over memory usage in the very least.

Unfortunately, no language I know of has a good concept of "strictness polymorphism" so in Haskell you end up with duplicate implementations of Strict and Lazy data structures. This ends up being not so much duplicated code, but a whole hell of a lot of duplicated API.

And I think the stream-cons/cons distinction is trivial. It's a lack of proper polymorphism that you're dealing with there and that can be easily implemented in any language with good polymorphism. In Haskell we have a very nice (very nice if you tolerate lenses, anyway, which you should) interface called Cons which is an elaboration of

    class Cons s where
      type Elem s
      _Cons :: Prism s (Elem s, s)
which works like this

    instance Cons [a] where
      type Elem [a] = a
      _Cons = ... -- more complex than worth explaining

    instance Cons (Stream a) where
      type Elem (Stream a) = a
      _Cons = ...
and then gives you

    cons   :: Cons s => Elem s -> s -> s
    uncons :: Cons s => s -> Maybe (Elem s, s)
which are generic in Stream a and [a].

Re: Haskell in the Large [pdf]

#92

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.

Yep - that's probably a fair way to describe it. It's of course possible in other statically typed languages, it's just not as easy. There are also some things that I'm not sure are reasonable at all in something like Java/C++ without writing a lot of code. For example: https://www.chrisstucchio.com/blog/2014/type_safe_vector_add...

I would say that it's not always possible. It's probably "possible" if you put about half the invariant in the type and half the invariant in documentation, of course, but that's a much weaker claim!

Java is in an interesting place in that its type system is rudimentary but not unpowerful. C is a more useful didactic target---there really do exist invariants which can be encoded in Haskell types but could never be encoded in C types!

Another huge target is parametricity. You can write Java code which is "maybe sort of parametric" but it really isn't and subsequently you can never trust it because of the existence of things like global reference equality and hash codes (in the least).

Finally, there are expressivity concerns. Java cannot encode as many things in its type language as something like Agda (to make a clear comparison). You can simply note that Java's type equality is nowhere nearly as developed as Agda's!

As an example of using Java to indicate a fairly non-trivial invariant and comparing that implementation to Scala, Haskell, and C# consider Tony Morris' challenge

http://tonymorris.github.io/blog/posts/understanding-practic...

Re: Haskell in the Large [pdf]

#93

I've toyed with Haskell, ultimately moving on to the Ocaml/F# camp. There are only two things that I miss from Haskell without an appropriate equivalent or easy workaround: Type Classes, and Higher Kinded Types. This big roadblock that everyone claims with Haskell, Monads, didn't give me any problems at all...even if it didn't make any sense to resort to them to do something as trivial as IO. What really turned me of…

The Windows-first status of F# is changing. There have been major improvements in this recently, most notably, the whole compiler being open sourced and its development moved to github[1], and .NET is going to be available on Linux[2]. This is not reality yet, but it will be during this year. [1] https://github.com/microsoft/visualfsharp [2] http://www.hanselman.com/blog/AnnouncingNET2015NETasOpenSour...

It is indeed not bad on unix. The only major flaw left is the lack of higher-kinded types.

Re: Haskell in the Large [pdf]

#94

Earlier quoted context omitted.

Haskell/Scala/etc makes it easy to nudge other developers into avoiding mistakes. A concrete example: I had a Scala system (build on Scalaz, which is a library providing Haskell for Scala), and one of our core types was DBTransaction[_] (a monad). A developer (a skeptic of the type system) was complaining to me about all the excess work he needed to go through, how he couldn't get properly construct a LazyStream[Foo]…

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.

Another way to think about it is kinda related to pg's stratified design. At the lowest level, you have things like system services, files, sockets, perhaps other processes. Regular old code may use those abstractions - or not - and build new stuff. for example parsers, matrixes, http responses, database connections.

Just like regular old code helps you manage the relationships between an input file and an output file, the type system helps you manage the relationship between libraries, or sets of functionality in your code. I don't care what type of data you pull from the database, but that type must agree with the type of matrix you're constructing. The parser may return a syntactically correct tree, or an error. One use of the type system is to ensure that all possible error conditions are handled in a meaningful way.

You can do this in java, but haskell's type system is a bit more expressive, so it's easier to enforce higher level constraints.

Another way to look at it, the type system is like the algebra axioms you want your system to follow. if equality is reflexive, a == b, then also b == a. At that level we don't care if a is 5 or "hello" or @TcpConnection(0x1342341a).

Re: Haskell in the Large [pdf]

#95
post #40
post #35

Earlier quoted context omitted.

> Monad stacks do wonders for circumscribing your computational context in an app. Wait until you discover the power of Applicative Functors. They are more restricted in their operations than Monads, so they compose better and allow for analysis.

I'm curious, what do you mean they compose better and allow for analysis [better than monads]?

gergoerdi covered analysis, but composition is simple. For any two Applicatives F and G and value type A the following 4 values are all Applicative values

    F A
    G A
    F (G A)
    G (F A)
But for monads only the first two are monads for general monads F and G. So, Applicatives compose better!

Re: Haskell in the Large [pdf]

#96
post #4

I wonder what's the primary reason for their "Mu" compiler adopting a "strict-ish" evaluation strategy.

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…

> One commonly cited benefit is a function that doesn't use all of it's arguments, therefore saving computation time when they're not evaluated. But realistically, an unused parameter should probably be removed.

How do you do that when the values of the other arguments determine whether or not that argument will be used?

Re: Haskell in the Large [pdf]

#97

Earlier quoted context omitted.

Haskell/Scala/etc makes it easy to nudge other developers into avoiding mistakes. A concrete example: I had a Scala system (build on Scalaz, which is a library providing Haskell for Scala), and one of our core types was DBTransaction[_] (a monad). A developer (a skeptic of the type system) was complaining to me about all the excess work he needed to go through, how he couldn't get properly construct a LazyStream[Foo]…

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 construct). This can allow you to easily enforce constraints like "A CreditCardNumber either had its parity validated OR does not exist". If you then put methods on an object that allow you to only manipulate the object in certain ways that maintain the constraints, there will exist no (direct) way to violate the basic constraints of the object.

This is reasonably powerful, and mastery of this technique is something that I would consider to be core to considering yourself at least a mid-tier professional developer.

However, there are many constraints you can not enforce in conventional languages. You can not enforce via type whether or not a given call will do IO or access global variables in unexpected manners. You can not enforce via type that a given method will only be called in a certain context (key in things like transactional memory, where you'd better be doing your STM things inside an actual transaction or the whole thing breaks down). You can not enforce whether an object will or will not be shared across thread boundaries. And so on, for a wide variety of additional guarantees that can be provided by a stronger type system. In the exciting-but-experimental world of dependent typing, you can enforce at the type system that a number is even or odd and stuff like that.

There are many different additional constraints being explored right now across a wide variety of languages, and while functional languages are leading the way, and there are some solid reasons for that, it isn't just functional languages that can use this... for instance, see Rust, which isn't functional at all in the modern sense but can still guarantee some of the things I said above.

(Rust, for instance, bring a question to the fore that I've been interested in for a while, but haven't had a major language to check it with: Is the important thing about functional programming immutability, or is it controlling mutation carefully? If in practice the latter is really what's important, than it is possible to see a set of "immutable" languages and see them successfully control mutation but accidentally attribute that to the "immutability", because that's the mechanism we happened to be using to accomplish the mutation control. I've already previously explained why I believe Erlang definitely had this problem: https://news.ycombinator.com/item?id=7744109 but with Rust we can explore whether Haskell has the right of the argument, or if Rust-style mutation control will turn out in practice to be sufficient. But it will be years before we can even start forming a decent answer... Rust needs some large scale programs and a body of people with experience writing large-scale Rust programs before we can even start forming a solid answer.)

Re: Haskell in the Large [pdf]

#98
post #75

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…

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 and not in C, but I was surprised by some of the things I could enforce in C with a little creativity.

Re: Haskell in the Large [pdf]

#99
post #4

I wonder what's the primary reason for their "Mu" compiler adopting a "strict-ish" evaluation strategy.

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…

an unused parameter should probably be removed.

It doesn't have to be completely unused to be avoided. In a case like:

if a then b + c else c + d

a and c are always evaluated, only b or d is evaluated not both. Removal isn't an option because b and d maybe used.

Re: Haskell in the Large [pdf]

#100

Earlier quoted context omitted.

Yep - that's probably a fair way to describe it. It's of course possible in other statically typed languages, it's just not as easy. There are also some things that I'm not sure are reasonable at all in something like Java/C++ without writing a lot of code. For example: https://www.chrisstucchio.com/blog/2014/type_safe_vector_add...

Thanks for the link. I've been wondering how to lift N-D operations into the type system. If I write with NumPy x = r_[:n].reshape((3, -1, n/15))[:, :2].sum(axis=-1) a compiler could figure out that the shape of x is (3, 2) and allow y = x + randn(m, 1, 2) while forbidding z = y - r_[:7] With NumPy you have to wait for a runtime error, and only if the shapes can't be broadcast. We're not even talking correct use of d…

I'm not sure what the notation you're using represents, but it looks like you're talking about matrices of a known size. What that's an example of is dependent types, where types can be parameterized by values, and not just types. For example, a (2D) matrix is parameterized by what it contains, and its dimensions. The former is a type but the latter are values. Without dependent types (or some subset of their capability) you can't represent this matrix type; you'd just have to check at runtime that no out-of-bounds access was occurring, so no; I don't think you could put this in a conventional language (without some crazy gymnastics, perhaps involving macros or similar). However, with dependent types, this is absolutely possible to statically guarantee that no out-of-bounds access will occur at runtime.
Post reply on HN