Live data from Hacker News

Dependent Haskell

serokell.io

91–92 of 92 posts

Re: Dependent Haskell

#91

Earlier quoted context omitted.

Comparing Haskell to brainfuck is a little hyperbolic -- you do not have fully understand Monads and their underpinnings to be productive in Haskell. Just like when new programmers write "public static void main" and have no idea what it does, or how JAR files work, or how cout works, newbies can type `do` and get off and running. In Haskell most of your time is spent writing non-monadic code -- writing pure function…

> you do not have fully understand Monads and their underpinnings to be productive in Haskell I don't think that's true. Most programming is done in a team, and someone will have written a transformer stack. I was told to use the free monad to solve my testing problem in my first Haskell program. "Hello world" doesn't count. > the difficulty contained within is fundamental to computation itself. Not always. The examp…

> I don't think that's true. Most programming is done in a team, and someone will have written a transformer stack. I was told to use the free monad to solve my testing problem in my first Haskell program. "Hello world" doesn't count.

Right but there isn't any other language where a production application will be obvious to newcomers anyway. There is always some cruft/enterprise design pattern/whatever else that will need to be learned or at least hand-waved for early productivity, and will be deeply understood later. My point was that you don't have to understand what "do" does. If you get some simple feature let's say update the user wiggle count when any friend wiggles), the chance you're going to be editing legible, clear haskell (given you understand how to read haskell) is high. Something like:

    -- | do a user wiggle and return the wiggle count 
    doWiggle :: User -> IO WiggleCount
    doWiggle user = do
        _ 
While this code is just a fake example, it's concise, and very legible -- you don't need to understand the complexities of the IO monad or any other stack that would be there, haskell can mimic the simplicity of a completely imperative monad-less environment, down to the `return`.

> Not always. The examples I gave are all of what I consider to be "unforced errors". I don't need monad transformers in any other language I've written code in. Or lens. Or arrows. Or free monads. Or...

But see this is the the whole point of the discussion of the relationship between lambda calculus and category theory. You're using most of these concepts already, you're just calling them something different, and wrapping them in some unnecessary ceremony/enterprise design pattern. Or even worse, you're using weaker, partial, worse approximations of these concepts and don't know it. Ignorance is not bliss in our line of work -- whether or not you use the concepts I (at least) expect good programmers to know the underpinnings.

> I did. Hence me even knowing what lens is.

I can't argue with your personal experience -- if you don't think learning that stuff was beneficial then there's nothing I could say to change your mind. My argument hinges on the fact that those concepts are beneficial and haskell shows them to you without much adulteration faster than other languages.

> Honest question: how is knowing Haskell's traversables (which are hard) going to add to one's knowledge if one has already worked with any of the following:

It adds to one's knowledge the same way knowing the Iterator/Iterable pattern exists instead of having used for loops in any of those patterns. It adds to one's knowledge the same way reading the gang of four book does, or any theoretical computer science does. Traversable is roughly identical to the iterator patterns but it is the purified form of the concept -- you don't get bogged down with how python iterates or some other language and how they built their iterator implementation.

> They wouldn't be able to. I say this as someone who somehow managed to take a student who didn't know how to add fractions together and tutor him to the point of (just) passing a university Linear Algebra class.

I don't consider myself an optimist, but I think you're wrong. If you were right, growth would be impossible for humankind. A more useful statement IMO might be that the amount of effort and focus one would have to put in is beyond what they could exert in the amount of time they have to devote (or their lifetime) -- but even then that's a hard statement to prove.

> So do I. Trying to learn Haskell was enlightening. I can't see me picking it as the tool of choice for pretty much any project though.

I mean that's OK though -- hopefully you picked up some things that were useful to you. Haskell ergonomics or practicality (basically, language features) is something that the Haskell community has to work on and make better.

> When I wrote Haskell I found myself working harder, writing bugs anyway and wondering what the point was. It's intellectually interesting, and worth looking into. I just don't want to write in it.

Again, I can't argue with your personal experience, but I can tell you that if you're using haskell's type system at all correctly what you're saying just can't be true. It's just not how it works -- for example, you probably have never gotten an NPE in Haskell -- it's a class of errors that doesn't exist for the most part. The errors you were getting (or maybe compiler feedback?) isn't the same as in other languages.

Re: Dependent Haskell

#92

Every discussion or article I have read on dependent types assumes that the reader is a mathematician. I usually make it only a few paragraphs in before I am completely lost. Right now the only thing that seems clear is that dependent typing adds significant mental burden on the programmer to more thoroughly specify types, and to do so absolutely correctly. In exchange for that burden, there must be practical (not th…

Indexing into a List

    sub lookup ( List \xs, Int \index ){…}
Make sure the index is valid.

    sub lookup ( List \xs, Int \index where 0 ..^ xs.elems ){…}
The `where` clause gets attached to the `Int` typecheck.

---

I think it may also apply if you have other limitations that you need to check regularly, like making sure that strings fit into a database.

    sub foo ( Str \name where .chars ≤ 256 ){…}
Which Perl6 has the ability to give that a name as if it was a type so that it can be reused.

    subset DB-Str of Str where .chars ≤ 256;

    sub foo ( DB-Str \name ){…}

    my DB-Str $name = '';

    $name = 'a' x 10000;
    # Typecheck error
---

One use of this feature is to implement the UInt type (This is almost exactly how it is implemented in the Rakudo implementation of Perl6)

    subset UInt of Int where {$_ >= 0};
---

Then again I've never read any that talk about Perl6 as already having that feature; so maybe I'm mistaken.

I would guess that they are talking about something slightly different. (That often seems to be the case)

Post reply on HN