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

Episode 21

Faith Evolution and Programming Languages, from Haskell to Java
Philip Wadler 

Faith and evolution provide complementary--and sometimes conflicting--models of the world, and they also can model the adoption of programming languages. Adherents of competing paradigms, such as functional and object-oriented programming, often appear motivated by faith. Families of related languages, such as C, C++, Java, and C#, may arise from pressures of evolution. As designers of languages, adoption rates provide us with scientific data, but the belief that elegant designs are better is a matter of faith. This talk traces one concept, second-order quantification, from its inception in the symbolic logic of Frege through to the generic features introduced in Java 5, touching on aspects of faith and evolution. The remarkable correspondence between natural deduction and functional programming informed the design of type classes in Haskell. Generics in Java evolved directly from Haskell type classes, and are designed to support evolution from legacy code to generic code. Links, a successor to Haskell aimed at AJAX-style three-tier web applications, aims to reconcile some of the conflict between dynamic and static approaches to typing.

Parametricity (Types are Documentation)
Tony Morris 

Philip Wadler tells us, Write down the definition of a polymorphic function on a piece of paper. Tell me its type, but be careful not to let me see the function's definition. I will tell you a theorem that the function satisfies.

Danielsson, Hughes, Jansson & Gibbons tell us, Functional programmers often reason about programs as if they were written in a total language, expecting the results to carry over to non-total (partial) languages. We justify such reasoning.

What does this mean and how might it be applied?

Parametric Execution Models
Daniel Spiewak

Among the small boatload of challenges facing developers of asynchronous software is that of testability.  It is very difficult to practically write concurrent algorithms which are then unit- and integration-tested in a repeatable fashion without relying on unreliable mechanisms like timeouts.  Furthermore, such systems are often very difficult to refactor in any significant fashion, due to the rigid hard-coding of the asynchronous mode of execution.  As one might expect, this is not merely a problem faced in concurrency, but rather an issue whenever an execution order or effect must be propagated through a series of computations while simultaneously remaining open to variant implementations.

This talk will explore the use of generic effects to abstract over the execution model of functions and even entire modules, allowing external constraints to drive the fundamental shape of the computation itself.  We will pay particularly close attention to some of the benefits these techniques can provide in the realm of testability and the ability to reason about our requirements at the type level.

Join or login to comment.

  • John K.

    Hi Everyone,

    Before the beginning of the presentation there were some short announcements regarding available Scala positions.

    One of them was an position at goCatch.

    To follow up on that announcement, a short Scala interview problem project is available that prospective job applicants can try out before applying.

    Happy hacking!

    January 21, 2014

  • Julian G.

    After Phillip Wadler's excellent talk - Mark Hibberd mentioned two additional Australian resources for further reading/watching on the topics that Phillip raised. Phillip pondered the question of whether you could communicate with aliens using Lambda Calculus.
    Manuel Chakrabarty answered this in his Lambdajam 2013 keynote:
    Do Extraterrestrials Use Functional Programming?

    In addition - Phillip made mention of work into Blame Calculus and its use in Type Inference in dynamically typed languages.
    This has been addressed in detail by an Australian named Ambrose BS who has been looking at adding types to Clojure via a type-checking function. A talk on this was given at clj-syd recently and it was written up by some guy.!topic/clj-syd/wslsA5gKGlk

    December 12, 2013

  • Matthew L.

    As Jed said 'Awesome'.

    December 12, 2013

  • Phil

    Great. Really enjoyed all the talks, all thought provoking. Daniel's improvisation, humor, music taste, intelligence and typing skills were all impressive. Phil Wadler and Tony Morris made Parametricity and type theory interesting and something to do more study on.

    1 · December 12, 2013

  • Arnold d.

    11 on the spinal tap awsome scale

    1 · December 11, 2013

  • Mark H.

    A brilliant night, entertaining and informative. Many thanks to the speakers (and typer!) for such standout presentations.

    1 · December 11, 2013

  • Sidney S.

    Great evening, lots of lightbulb moments from the presentations.

    December 11, 2013

  • Tibo D.

    Wow, that's a pretty impressive set of talks! Really looking forward to it

    1 · November 29, 2013

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