schedule May 13th 08:30 AM - 04:30 PM place Room 1 shopping_cart Reserve Seat

Let's Lens presents a series of exercises, in a similar format to the Data61 functional programming course material. The subject of the exercises is around the concept of lenses, initially proposed by Foster et al., to solve the view-update problem of relational databases.

The theories around lenses have been advanced significantly in recent years, resulting in a library, implemented in Haskell, called lens.

This workshop will take you through the basic definition of the lens data structure and its related structures such as traversals and prisms. Following this we implement some of the low-level lens library, then go on to discuss and solve a practical problem that uses all of these structures.

 
2 favorite thumb_down thumb_up 0 comments visibility_off  Remove from Watchlist visibility  Add to Watchlist
 

Learning Outcome

An attendee who completes this workshop should expect to confidently use the lens library, or other similar libraries, in their every day programming.

Target Audience

All

schedule Submitted 1 month ago

Public Feedback

comment Suggest improvements to the Speaker

  • Liked Philip Wadler
    keyboard_arrow_down

    Philip Wadler - (Programming Languages) in Agda = Programming (Languages in Agda)

    60 Mins
    Keynote
    Beginner
    The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that propositions
    correspond to types, proofs to programs, and simplification of proofs to evaluation of programs. The proof of a conjunction is a pair, the
    proof of a disjunction is a case expression, and the proof of an implication is a lambda expression. Proof by induction is just programming by recursion.
    Dependently-typed programming languages, such as Agda, exploit this pun. To prove properties of programming languages in Agda, all we
    need do is program a description of those languages Agda. Finding an abstruse mathematical proof becomes as simple and as fun as hacking a
    program. This talk introduces *Programming Language Foundations in Agda*, a new textbook that is also an executable Agda script---and also explains the role Agda is playing in IOHK's new cryptocurrency.
  • Liked Edward Kmett
    keyboard_arrow_down

    Edward Kmett - Logic Programming à la Carte

    30 Mins
    Talk
    Beginner
    I've been working on a logic programming framework in Haskell, called guanxi (關係) with an eye towards scalability. To build it I leaned heavily on my previous work on propagators and a bunch of other little bits and pieces of algebra and category theory in the design process. A number of patterns have arisen repeatedly throughout the process of building this library. I'll give a tour through the current state of guanxi and try to extract some of the more reusable bits of its design for your inspection.
  • Liked Xuanyi Chew
    keyboard_arrow_down

    Xuanyi Chew - An Alien Lambda Calculus

    Xuanyi Chew
    Xuanyi Chew
    Chief Data Scientist
    Ordermentum
    schedule 1 day ago
    Sold Out!
    30 Mins
    Talk
    Beginner

    The conventional wisdom in functional programming communities is that lambda calculus was "discovered". Extending the logic of the statement to its extreme, we might propose that an alien would recognize lambda calculus as a computational model. But would we be able to recognize an alien lambda calculus?

    This talk is part gedankenexperiment, part speculative fiction, part practical advice on compiler design. We begin by imagining ourselves to be creatures in a universe which is very different from the one we're in, except the notion of consciousness and intelligence are preserved from our current universe. From there, we shall explore the physics and alternate philosophies that would yield an alien lambda calculus.

    Of course, being from an alien conception, there are some questions that must be answered - in the name of practicality, is there perhaps even a weak notion of a functor from the alien lambda calculus to that of the one we know today? Is there anything from the alien lambda calculus that we may yield and put into practice? And what is this pesky business with state? Isn't the point of functional programming to hide states from the programmer by abstracting over them? Or was it to make clear the states? And what of names? Isn't lambda purely anonymous?