addressalign-toparrow-leftarrow-rightbackbellblockcalendarcameraccwcheckchevron-downchevron-leftchevron-rightchevron-small-downchevron-small-leftchevron-small-rightchevron-small-upchevron-upcircle-with-checkcircle-with-crosscircle-with-pluscrossdots-three-verticaleditemptyheartexporteye-with-lineeyefacebookfolderfullheartglobegmailgooglegroupshelp-with-circleimageimagesinstagramlinklocation-pinm-swarmSearchmailmessagesminusmoremuplabelShape 3 + Rectangle 1ShapeoutlookpersonJoin Group on CardStartprice-ribbonShapeShapeShapeShapeImported LayersImported LayersImported Layersshieldstartickettrashtriangle-downtriangle-uptwitteruserwarningyahoo

General discussion

Haskell, Haskell, Haskell! This is an open discussion for anything Haskell-related.

Join the message boards to participate in our online discussion!

Join or login to comment.

  • Richard G.

    I asked a question toward the end of the meetup that was unfortunately very vague, so I'd like to clarify it (and hopefully get a better answer) here.

    In the software industry currently, our best and most reliable way to verify program behavior is through testing: unit tests, integration tests, etc. As we know from experience, while tests are better than no tests, you can only guarantee so much about program behavior with them. How would this story change with dependent types? Would we convert tests to proofs? What behavior would require testing as we do it today even with dependent types?

    3 days ago

    • John L.

      I could go on for a while about this, but relatively briefly.... I would say that right now we attempt to verify software behavior via a combination of static analysis (for example type checking), dynamic analysis (for example runtime array bounds checking) and testing. Static analysis is the best of the three since you can guarantee correctness (which testing cannot unless it is exhaustive) and it doesn't have runtime overhead.

      With dependent types it is possible to specify the type so precisely that the program, if it typechecks, must meet the specification. So theoretically you no longer need the other two. However in practice it may be so difficult to specify this precise type that you opt for a weaker type and rely on dynamic analysis and/or testing to fill in the gaps. Another issue is that your spec might be wrong, so it can be good to retain tests as a sanity check.

      2 days ago

    • John L.

      John Hughes who invented quickcheck and has a commercial version for Erlang talked about how he found several errors in specifications for software components for automobiles, a main area he is working on.

      Check out the DeepSpec project which is particularly ambitious and addresses these issues, including testing.

      2 days ago

  • John L.

    Thanks everyone for your comments, and especially Ashley for the suggestion that F₁Id could be simplified. I've made the change and pushed it. I'd still be interested if anyone can figure out how to use the intensional versions of F₁Id and F₁Comp that are commented out and prove F₁Comp for functor composition. The intensional versions are less elegant, but this would remove the necessity of postulating function extensionality.

    1 · 6 days ago

  • John L.

    I'd like to go into more detail on some aspects I rushed over last month relating to functor decomposition of Parser, and possible implications for support for dependent types in Haskell. A half hour to an hour, depending on how much audience participation there is.

    I'd also like to reserve an hour slot for the March meeting. I'm going to BayHac in April and will give a half-hour talk (with slides) on Dependent Types in GHC. I'd like to practice here with a friendly audience, of course!

    February 10

  • John L.

    Materials for my presentation this month are here:
    https://github.com/halfaya/Seahug/

    February 17

  • Richard C.

    Hello, everyone! Here's a tentative agenda for our 18 February meeting:

    Tom Guo "Monoidal Presentation of Applicative Functors" (approx. 20 minutes + 10 minutes' discussion)
    Jay Coskey "Derivatives of Regular Types and Related Type Operations" (approx. 50 minutes + 10 minutes' discussion)

    So, that should leave plenty of time for other topics. Please post with suggestions or PM/e-mail me. Thanks!

    February 9

Our Sponsors

People in this
Meetup are also in:

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy