Events

Feed icon 28x28
Small lambdaconf original

LambdaConf 2015 Schedule

May 22 - 23, 2015

( 58 available presentations )
Untitled thumb
Rating: Everyone
Viewed 99 times
Recorded at: May 15, 2015
Date Posted: January 11, 2016

Rust aims to build a solid foundation for building safe software systems faster. We can ensure fewer mistakes enter our code base with immutability by default, no concept of null, and proven memory safety. Rust's state of the art compiler helps developers catch errors as early as possible without paying a penalty at runtime. Developers can write high level code in a modern language without sacrificing expressiveness, development time, or execution speed. We will explore how Rust's concept of Ownership is the key to providing compile-time safety. These guarantees apply even in the face of concurrency, allowing you to easily write multi-threaded programs correctly the first time. Rust 1.0 was released May 15th. Start building better software today.

Vlcsnap 2015 12 29 14h32m30s586 thumb
Rating: Everyone
Viewed 162 times
Recorded at: May 15, 2015
Date Posted: January 4, 2016

"Compatibility means deliberately repeating other peoples' mistakes," said Wheeler. Not only a pithy aphorism, but literally true. And today, almost fifty years after the birth of unix, we still make it a point to deliberately repeat mistakes - even if we don't count unix itself among them. Why do we still program to teletypes? Why must we concern ourselves with newlines in file names? Why is it still an everyday occurrence to find the arrow keys don't work? Why did scala intentionally repeat most of java's mistakes? How is it that so much effort is poured into validation of inputs, yet it's never enough? How can it be that we know the benefits of types, yet only enjoy those benefits in a minority of environments? Why is it so difficult to clamber above the maelstrom of complexity - and stay there? Can't we have it both ways - make improvements without sacrificing compatibility? In fact, we can have it both ways. The subject of my talk is the almost unexplored frontier through which we can disrupt the endless perpetuation of mistakes of the past: ipecac for the ouroboros.

Untitled thumb
Rating: Everyone
Viewed 100 times
Recorded at: May 15, 2015
Date Posted: January 11, 2016

Many machines and devices come equipped with powerful graphical processing units, or GPUs. These units have hundreds of processing cores, and can be exploited to accelerate our applications by offloading applicable code to the GPU instead of the CPU. In this talk we will cover the basic concepts of General Purpose Programming for GPUs, and show how it can be exploited in the functional programming language, Haskell, via the accelerate library.

Vlcsnap 2015 12 29 14h28m49s814 thumb
Rating: Everyone
Viewed 94 times
Recorded at: May 21, 2015
Date Posted: December 30, 2015

This workshop will give an introduction to Typed Racket. We will give an overview of the features of its type system, go over some examples of typing old untyped Racket code and provide some accompanying typing exercises for people to try. We will also discuss some current issues trusting Typed Racket, e.g. sketchy examples of mixing typed and untyped code. Finally, we will discuss the need to add type annotations to a significant number of existing Racket modules - and try to get people interested in contributing to Typed Racket. Some prior experience using a Lisp-like functional programming language, such as Scheme/Racket, could be an asset in understanding the content of this workshop, though none is required.

Vlcsnap 2015 12 29 13h09m00s130 thumb
Rating: Everyone
Viewed 172 times
Recorded at: May 21, 2015
Date Posted: December 30, 2015

Idris is a dependently typed programming language. Unlike most other dependently typed systems, Idris is designed specifically for writing executable programs. This workshop will slowly walk through writing a few programs using dependent types, to motivate its uses around correctness and expressivity. This workshop will be modeled similarly to LambdaConf 2014's but with new examples to demonstrate what Idris is capable of. The only prerequisite knowledge is familiarity with algebraic data types. It is important to have the Idris REPL installed, optionally with an interactive editor configuration such as Emacs' idris-mode or Vim's idris-vim.

Vlcsnap 2015 12 29 13h15m20s154 thumb
Rating: Everyone
Viewed 174 times
Recorded at: May 21, 2015
Date Posted: December 30, 2015

Program Derivation is the practice of beginning with a specification of a function, and by a series of mechanical steps, deriving an efficient implementation. In the “Algebra of Programming” approach, pioneered by Richard Bird, Oege de Moor, and Lambert Merteens, we can derive efficient functional programs by a series of algebraic manipulations, much schoolchildren can take a typical algebraic function, “solve for x” and then simplify. In the early-mid 90s, this school of research turned its attention to the problem of parallel computing and developed many of the foundations for what is now called MapReduce. This workshop will run through some famous and nifty algorithms and derivations, parallel and sequential alike. Attendees should walk away with a few weird tricks to level up their equational reasoning in everyday programming contexts, and hopefully enough intuition to dive more deeply into this rich body of literature.

Vlcsnap 2015 12 29 13h08m37s413 thumb
Rating: Everyone
Viewed 42 times
Recorded at: May 21, 2015
Date Posted:

Web development is easy and fun with Haskell... and of course, type safe! Let's take a birds-eye tour on creating a web application in Haskell from scratch, from the initial project creation to deployment in the cloud. By the end of the workshop, you will have deployed a small server for note-taking. The workshop is divided in four slots, each dealing with a different facet of web development. First of all, simple routing and building of HTML to be returned to the clients. Then, adding database capabilities using Persistent and Esqueleto. The next step is taking input from the user via digestive functors. Finally, deployment to Heroku will be considered, along with integrating other middleware in your application.

Vlcsnap 2015 12 29 13h08m30s973 thumb
Rating: Everyone
Viewed 62 times
Recorded at: May 21, 2015
Date Posted: December 29, 2015

A burgeoning Haskeller soon discovers that proper use of descriptive types helps to capture real-world ideas, catches errors, aids in refactoring, speeds development, and indeed makes programming more fun. But, once that Haskeller has drunk the well-typed Kool-Aid, where to go from there? The answer: even more types! A Generalized Algebraic Datatype (GADT), at its core, allows a compiler to make different assumptions about types within different branches of a pattern match. Leveraging this power allows a programmer to encode detailed invariants in a datatype or algorithm and have these invariants checked at compile time. Clever use of GADTs also lets you remove certain uses of unsafeCoerce, as long as these can be proved safe. This workshop will be a hands-on, interactive tutorial on using Haskell GADTs in a practical setting.

Vlcsnap 2015 12 29 14h28m32s891 thumb
Rating: Everyone
Viewed 95 times
Recorded at: May 21, 2015
Date Posted: December 30, 2015

Constraint logic programming is a paradigm that allows solving hard combinatorial problems with minimal programming effort. In this workshop you will learn the basics of the Prolog-based constraint logic programming system ECLiPSe, solve several puzzles, and get hints how constraint logic programming can be useful in your real-life projects.

Vlcsnap 2015 12 29 13h08m46s111 thumb
Rating: Everyone
Viewed 30 times
Recorded at: May 21, 2015
Date Posted: December 30, 2015

Haskell has many delightful features, perhaps the most beloved of which is its type system which allows developers to specify and verify a variety of program properties at compile time. However, many properties, typically those that depend on relationships between program values are impossible, or at the very least, cumbersome to encode within Haskell's type system. Refinement types enable the specification and verification of value-dependent properties by extending Haskell's type system with logical predicates drawn from efficiently decidable logics. In this talk, we will start with a high level description of Refinement Types. Next, we will present an overview of LiquidHaskell, a refinement type checker for Haskell. In particular, we will describe the kinds of properties that can be checked, ranging from generic requirements like like totality (will 'head' crash?) and termination (will 'mergeSort' loop forever?), to application specific concerns like memory safety (will my code 'SEGFAULT' ?) and data structure correctness invariants for various libraries like containers, hscolour, bytestring, text, vector-algorithms and xmonad.

Vlcsnap 2015 12 29 14h28m39s544 thumb
Rating: Everyone
Viewed 111 times
Recorded at: May 21, 2015
Date Posted: December 30, 2015

If you have heard nothing else about Erlang, you have probably heard something about OTP and people chanting “Processes are not threads. Processes are really cheap. Ohmmmm.” In this workshop you will get a overview of Erlang syntax, OTP process management, and how cheap Erlang processes really are when you implement a Markov Chain generator where each state and its possible transitions are represented by their own process.

Vlcsnap 2015 12 30 11h20m58s156 thumb
Rating: Everyone
Viewed 185 times
Recorded at: May 22, 2015
Date Posted: December 30, 2015

In this talk, Paul Phillips expands on ideas in his keynote to deliver a compelling vision for how properly conceived and implemented virtual file systems have the ability to literally change every single thing about how we interact with computers.

Vlcsnap 2015 12 29 14h30m00s541 thumb
Rating: Everyone
Viewed 125 times
Recorded at: May 22, 2015
Date Posted: December 30, 2015

"Programming in Scala", by Martin Odersky et al., is one of the most comprehensive and the de facto reference for Scala. However, the book, originally published in 2008 for Scala 2.7.2, has not been updated since its second edition in 2010, covering up until Scala 2.8.1. In the meantime, Scala has had 3 major releases with numerous fresh and advanced features. While we wait for a third edition of "Programming in Scala" to describe all the latest and greatest Scala features introduced in the last 4 years, this talk presents the main features introduced in Scala: 2.9, 2.10, and 2.11, as well as an exciting peek into 2.12 and beyond (What's in Scala's future?).

Vlcsnap 2015 12 29 13h17m20s112 thumb
Rating: Everyone
Viewed 136 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

Writing correct concurrent, fault-tolerant, scalable applications is no simple task. The struggle is generally the result of using the wrong tools or wrong level of abstraction. The Actor based concurrency model aims to simplify this process. The actor model is a mathematical model of concurrent computation originated in 1973 by Carl Hewitt, Peter Bishop, and Richard Steiger. Actor programming is one of the most widely applicable programming models, which provides support for concurrency, by improving distribution, error detection, and fault tolerance. As such, it’s a good fit for the kinds of programming problems we find ourselves faced with in today’s increasingly distributed world Actors raise the abstraction level and provide a better platform to build correct concurrent and scalable applications. This presentation will introduce concepts in architecture such as immutability, isolation and asynchronous processing utilizing tools such as Akka.NET which is a .NET port of the popular JVM framework Akka. The goal is to provide solid knowledge of and foundation for the Actor model. Following the presentation, attendees will take with them enough material to start to use and leverage the Actor model to write successful concurrent applications.

Vlcsnap 2015 12 29 13h10m58s425 thumb
Rating: Everyone
Viewed 81 times
Recorded at: May 22, 2015
Date Posted: December 31, 2015

“Programming is about abstraction.” But what is abstraction about? Surely not just programming. Why do we need it, why do we keep reinventing it? How do we even recognize it when we see it, across so many domains? When something is more abstract, it is not necessarily more useless, even though, definitionally, it is further removed from any specific use. How can that even be the case? Too often, when we teach functional programming, we are met with the response “you have taught me some abstractions, but not what they are good for.” Certain realms of mathematics, such as category theory, often elicit similar responses. This talk is an investigation into how to consider not only abstractions, but the process of applying them.

Vlcsnap 2015 12 29 13h13m52s969 thumb
Rating: Everyone
Viewed 1,352 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

Rust aims to build a solid foundation for building safe software systems faster. We can ensure fewer mistakes enter our code base with immutability by default, no concept of null, and proven memory safety. Rust's state of the art compiler helps developers catch errors as early as possible without paying a penalty at runtime. Developers can write high level code in a modern language without sacrificing expressiveness, development time, or execution speed. We will explore how Rust's concept of Ownership is the key to providing compile-time safety. These guarantees apply even in the face of concurrency, allowing you to easily write multi-threaded programs correctly the first time. Rust 1.0 was released May 15th. Start building better software today.

Vlcsnap 2015 12 29 14h33m46s318 thumb
Rating: Everyone
Viewed 228 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

Shortly after Adelbert Chang entered college as a computer science major, he contemplated changing his major several times, usually in the direction of physics and mathematics. That all changed when he was introduced to functional programming — at once both mysterious and beautiful. In this talk, Adelbert will elaborate on his early perspectives on computer science, math, and physics, and discuss how he ended up so enamored with functional programming.

Vlcsnap 2015 12 30 11h20m45s25 thumb
Rating: Everyone
Viewed 82 times
Recorded at: May 22, 2015
Date Posted: December 30, 2015

Operations on power series showcase the elegance and expressiveness of overloading and lazy evaluation. Simple one-liners for sum, product, integral, derivative, functional composition, functional inverse, etc. vividly embody the underlying mathematics, and even improve upon it by banishing subscripts. Series solutions of differential equations come practically for free and generating functions actively generate.

Vlcsnap 2015 12 29 13h14m27s165 thumb
Rating: Everyone
Viewed 152 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

Free monads, generic programming, fix-points and coproducts of data types are usually considered advanced topics for a Haskell programmer. In this talk we will look at these concepts from an unifying lens: combining and enriching pattern functors. A pattern functor is the stripped-down description of a data type: only the shape of the constructors remain, but all the recursive structure is gone. Using Haskell, we can manipulate pattern functors to create new data types at will.

Vlcsnap 2015 12 29 13h16m11s987 thumb
Rating: Everyone
Viewed 1,366 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

What happens when we prototype an app entirely in FP? From choosing a functional database to building http apis and designing templates and stylesheets—it is possible these days, to stay entirely in FP land! In this talk I will share my experience in building functional prototypes with Clojure & Clojurescript using the following libraries: Datomic, Ring, Om, and Garden. I’ll discuss how we can trade popular databases, web toolkits, template engines, and even less and sass in favor of simpler libraries that embrace immutable data as a “Sequence of Values”.

Vlcsnap 2015 12 29 14h30m00s541 thumb
Rating: Everyone
Viewed 158 times
Recorded at: May 22, 2015
Date Posted: December 30, 2015

The Scaladoc page for Option says: "The most idiomatic way to use a scala.Option instance is to treat it as a collection or monad and use map, flatMap, filter, or foreach [...] A less-idiomatic way to use scala.Option values is via pattern matching." In this talk we show how to use the Option monad in an idiomatic, functional style, leveraging its comprehensive set of higher-order functions to solve any coding situation in a concise and declarative manner. After this talk, you will never have to pattern match against Options again!

Vlcsnap 2015 12 29 14h29m23s161 thumb
Rating: Everyone
Viewed 84 times
Recorded at: May 22, 2015
Date Posted: December 31, 2015

We've all seen them on the corner of our local software development neighborhoods: FP purists, shamelessly peddling scalaz to unsuspecting developers. Lured in by promises of Free Monoids, Semigroups, and Endofunctors these developers soon seem lost in throes of ecstatic coding. To the skeptical and stubbornly practical among us, the above might ring a little true – especially if read in Rod Serling's voice. Images of gibbering horrors lurking in the depths of mathematical perfection swim before our eyes. But what if there is true value in the world of Scalaz? What if it is possible to use these tools for good (and a little bit of evil – it's fun to use learning for evil!) and profit... Without getting hopelessly lost in the opium dens of FP? In this talk we will look at some of the "gateway drugs" of Scalaz: Validation, NonEmptyList, \/, Monad Transformers, and more. How do they work from a practical standpoint? What is their value for real world applications? Can we use them without an advanced Maths PhD? And just how fun is it to really code with these tools?

Vlcsnap 2015 12 29 14h35m00s437 thumb
Rating: Everyone
Viewed 95 times
Recorded at: May 22, 2015
Date Posted: December 30, 2015

There are patterns for modeling data that are not obvious or widely covered in Haskell that only require the application of basic algebraic datatypes, we'll explore some of these approaches with the dual purpose of introducing thinking in terms of algebraic datatypes in Haskell. The audience is not expected to know Haskell.

Vlcsnap 2015 12 29 13h15m58s706 thumb
Rating: Everyone
Viewed 277 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

Types remain a highly contentious issue for programmers in industry. Rails and Python have massive communities, and drive high-profile, high-traffic, successful businesses, such as GitHub, Reddit, and Dropbox. Clearly, dynamic languages are a better choice than Java or C; unless, of course, we count the myriad more businesses powered by 90s statically typed languages (e.g. Java). This statement will infuriate some engineers and academics, as we all know that Hindley-Milner type systems are the only type systems that reduce defects and improve code quality. In this talk, we'll take a look at type systems through a different lens: how type systems are actually a business decision that is frequently cast as an emotional decision.

Vlcsnap 2015 12 29 14h30m33s138 thumb
Rating: Everyone
Viewed 335 times
Recorded at: May 22, 2015
Date Posted: December 30, 2015

Scalaz is a massive library full of many critical FP abstractions, but it can be a bit dense. If you've dipped into Scalaz for a couple things such as Either and Validation, but you're not sure what else you can use, this talk is for you!

Vlcsnap 2015 12 29 13h13m45s826 thumb
Rating: Everyone
Viewed 112 times
Recorded at: May 22, 2015
Date Posted: December 31, 2015

The Haskell community is often abuzz about free monads and if you stick around for long enough you'll also see notions of free monoids, free functors, yoneda/coyoneda, free seminearrings, etc. Clearly "freedom" is a larger concept than just Free f a ~ f (Free f) + a. This talk explores briefly the origins of "freedom" in Category Theory, explains what it means for you to have a "free X" for any thing X, and talks a little bit about some useful free structures which exist in Haskell.

Vlcsnap 2015 12 29 14h32m12s022 thumb
Rating: Everyone
Viewed 335 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

Haskell is known for being hard, this is a result of pedagogy catching up to different ways of thinking about and structuring programs. We can make teaching ourselves and others something that is not only more effective, but enjoyable in its own right.

Vlcsnap 2015 12 29 14h35m13s786 thumb
Rating: Everyone
Viewed 200 times
Recorded at: May 22, 2015
Date Posted: December 30, 2015

We spend all day communicating with people - verbally, nonverbally, on social media, over the phone, and in a myriad of other ways. But have you noticed that even though we are always connected to people, we aren't every really connecting with people? As a stutterer I know the struggle to effectively get your point across, especially in a time-crunched society. We as humans are rushed, rarely patient and generally in transit to the next thing. And I understand; I spend just as much time flying through the day as the next person. But I also understand the value of human interaction, and the fear that comes along with the idea of it. I've tried - and failed - at having meaningful conversations many times because of fear that I won't be accepted for who I am. But once I opened myself up to potential rejection, I ended up being accepted and celebrated for being flawed. Let's explore that fear together: the fear of reaching out, of real conversations and of willingly extending our hand to others looking to truly connect with us. Our weaknesses are often times great compliments to our strengths; it's time to be inspired to embrace vulnerabilities, empower our weaknesses and truly connect with the human beings around us.

Vlcsnap 2015 12 29 14h34m47s355 thumb
Rating: Everyone
Viewed 93 times
Recorded at: May 22, 2015
Date Posted: December 30, 2015

Hole-driven Development with GHC-mod - Alejandro Serrano Mena

Code Literacy is Literacy Too - Gershom Bazerman

Feel the Rush: CRDTs in Riak - Zeeshan Lakhani

An ARM-Powered Musical Instrument Using Haskell - Ben Burdette

Trampolines and Lifting: AKA Save Your Stack - Vincent Marquez

A Microservices Architecture with Haskell: An Experience Report - Phil Freeman

Vlcsnap 2015 12 29 13h42m08s532 thumb
Rating: Everyone
Viewed 92 times
Recorded at: May 22, 2015
Date Posted: December 30, 2015

Part 2
Freya is a stack of libraries for F# which are designed to let you get close to HTTP in a functional, typed way. As well as providing a useful set of abstractions over HTTP, it also offers a graph based approach to modelling HTTP responses, enabling the creation of "well-behaved" HTTP applications simply (and correctly). We'll take a tour through the stack and exercise the various parts individually, before diving in to write a complete HTTP application. We'll see how easy it is to write applications which take full advantage of the HTTP standards, and then we'll look at ways of extending our application out past the world of RFCs in to the world of hypermedia - and we'll do it with graphs! After this session you'll be comfortable building an application using Freya, and you'll almost certainly have come up with some great ideas for how Freya, and the graph based approach to logical design, could be extended to do even more.

Vlcsnap 2015 12 29 13h42m08s532 thumb
Rating: Everyone
Viewed 77 times
Recorded at: May 22, 2015
Date Posted: December 30, 2015

Freya is a stack of libraries for F# which are designed to let you get close to HTTP in a functional, typed way. As well as providing a useful set of abstractions over HTTP, it also offers a graph based approach to modelling HTTP responses, enabling the creation of "well-behaved" HTTP applications simply (and correctly). We'll take a tour through the stack and exercise the various parts individually, before diving in to write a complete HTTP application. We'll see how easy it is to write applications which take full advantage of the HTTP standards, and then we'll look at ways of extending our application out past the world of RFCs in to the world of hypermedia - and we'll do it with graphs! After this session you'll be comfortable building an application using Freya, and you'll almost certainly have come up with some great ideas for how Freya, and the graph based approach to logical design, could be extended to do even more.

2 thumb
Rating: Everyone
Viewed 234 times
Recorded at: May 22, 2015
Date Posted: January 5, 2016

Finally Tagless DSLs are a DSL embedding technique pioneered by Oleg Kiselyov, Jaques Carrette, and Chung-Chieh Shan that is in some sense "dual" to the notions of free-monad interpreters. MTL is a very popular monad library in Haskell which just so happens to be, unbeknownst to most, a Finally Tagless DSL itself. This talk explores what the Finally Tagless DSL style offers and shows you can use that concept to extend your effect-typing vocabulary in MTL.

Vlcsnap 2015 12 29 14h29m38s611 thumb
Rating: Everyone
Viewed 297 times
Recorded at: May 22, 2015
Date Posted: December 31, 2015

Cats is a library that aims to fill in the gaps in the Scala standard library that we think are necessary to do pure functional programming in Scala, in the same way that Scalaz attempts to fill the same role. This project intends not only to create a functional library, but it intends to create a community welcoming to all. Having the opportunity to start on a library like this from scratch gives us many delicious opportunities to rethink some past decisions, and this is allowing us to innovate in unexpected ways.

Vlcsnap 2015 12 29 13h16m31s829 thumb
Rating: Everyone
Viewed 146 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

Object-oriented Programming (OOP) dominates the industry. Most developers have experience with OO, but are new to functional programming. To help bring them to functional programming, we developed ooErlang, an extension of Erlang that fully supports OO with simpler syntax than previous approaches. This talk presents how we have implemented ooErlang and how to start using it.

Vlcsnap 2015 12 29 14h33m11s509 thumb
Rating: Everyone
Viewed 200 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

Design patterns are a useful way to organize software. Unfortunately, "gang-of-four"-like patterns are not composable, due to side-effects. In a pure (i.e., no side-effects) language, functions can be composed. That makes it possible to leverage patterns from mathematics. This talk shows an algebra of function composition, identity functions, isomorphisms, (co)products (gluing functions that do not compose) and functors. It shows how this algebra relates to real-world programming. The goal of this talk is to provide an initial intuition of how to apply patterns from math to programming and to motivate you to continue studying on your own (perhaps by looking at the "uber" patterns of Category Theory). Note: knowing these patterns is NOT necessary for getting work done in a functional language, but this talk should give a glimpse of why they may be useful. The talk illustrates ideas using Haskell. It is aimed at FP beginners.

Vlcsnap 2015 12 29 14h34m36s143 thumb
Rating: Everyone
Viewed 105 times
Recorded at: May 22, 2015
Date Posted: December 30, 2015

This workshop is designed for programmers of any skill level who want to learn functional programming. PureScript is ideal for learning functional programming, because the language has simple, clean semantics, and runs on any platform because it compiles to ubiquitous Javascript. In this workshop, you'll learn what it means to think functionally and write functional code as you explore the core concepts in PureScript. By the end, you'll have written your first functional program (a simple game!) and be able to call yourself a rookie functional programmer.... or else the instructor promises to buy you a coffee!

Vlcsnap 2015 12 29 14h30m38s867 thumb
Rating: Everyone
Viewed 155 times
Recorded at: May 22, 2015
Date Posted: December 30, 2015

[serious announcer voice] In a world gone mad with data, one library stands alone in the fight against sloppy, unsafe processing. [/serious announcer voice] The scalaz-stream library brings type safety, flexibile composition and powerful abstractions to the world of streaming data processing. This talk will start out with the basic building blocks and move on to advanced techniques, covering the good, bad, and the ugly along the way.

Vlcsnap 2015 12 29 14h34m27s397 thumb
Rating: Everyone
Viewed 230 times
Recorded at: May 22, 2015
Date Posted: December 30, 2015

Cryptol is an open source pure functional language for expressing and reasoning about bit-precise computations, particularly cryptographic algorithms. Like Haskell, it is built upon a polymorphic, static type system, and offers similar mathematical function and sequence comprehension notation. The type system features size polymorphism and arithmetic type predicates designed to express the constraints that naturally arise in cryptographic specifications. The advanced type system and restricted domain of Cryptol enables a theorem-driven development style: correctness properties can be expressed directly in the language in tandem with the development of a specification. As the specification evolves, these properties can be continually fuzz-tested with random QuickCheck-style testing, and even sent to external SAT and SMT solvers for a mathematical proof of correctness. In this workshop, I’ll give a quick introduction the Cryptol language geared toward folks with a working knowledge of typed functional programming. Together we will implement a classical cryptosystem to learn the basic syntax and semantics of the language. As we program, we will express and check correctness properties about our implementations using QuickCheck and SMT. Finally, I will demonstrate a Cryptol specification of the ZUC stream cipher used in 4G LTE communications, and show how the theorem-driven development approach reveals a bug that required a revision of the cipher.

Vlcsnap 2015 12 29 13h16m24s009 thumb
Rating: Everyone
Viewed 153 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

We're all used to typing code into an editor and seeing the computer do something when we run it. This is so familiar that it's easy to take for granted. How do we go from a sequence of characters to something the machine can execute? Knowing this will not only help you program more effectively, but it will empower you to create your own programming languages. I'll give an overview of the pipeline from your text editor to the machine's behavior. Then, we'll dive in and look at specific tools that will help us create our own programming language. We'll also discuss different language design decisions, such as static versus dynamic typing, and see how they are implemented behind the scenes. By the end, you'll be ready to bring your new language into the world!

Vlcsnap 2015 12 29 14h32m55s245 thumb
Rating: Everyone
Viewed 130 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

This introductory talk is designed to help students new to functional programming understand how type parameters enable us to more easily reason about the behavior of functions and create APIs that enforce their invariants with type-level constraints. We will cover the principles of universal and existential quantification, review examples of reasoning about behavior from function types, and discuss implications for compositionality in API design. While most examples will be in Haskell, we will discuss how the principles generalize even to code written in unityped languages.

Vlcsnap 2015 12 29 14h32m48s931 thumb
Rating: Everyone
Viewed 57 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

When entering the world of functional programming, one is quickly introduced with a concept of a Monad. Concept that is for some reason really hard to grasp and comprehend. When querying the Internet for "What is a Monad?" you will most likely learn that "you do not need to know the category theory to understand monads" and that "you are not asking the right question". The first thing that came to my mind, when I was struggling with this dilemma, was "Well, what is the right question then?". This talk is all about looking for that right question and answering it. After this talk I hope you will find yourself knowing and understanding the concept, being able to apply it in a daily programming routine.

Vlcsnap 2015 12 29 14h32m39s104 thumb
Rating: Everyone
Viewed 63 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

Graphs are ubiquitous data structures, and the algorithms for analyzing them are fascinating. Loom is an open-source Clojure library that provides many graph algorithms and visualizations. We will discuss how graphs are represented in a functional world, bridge the gap between procedural description of algorithms and their functional implementation, and learn about the way Loom integrates with other graph representations.

Vlcsnap 2015 12 29 14h29m51s021 thumb
Rating: Everyone
Viewed 77 times
Recorded at: May 22, 2015
Date Posted: December 31, 2015

Computation Expressions are a generalization of do-notation and Idiom Brackets. They provide a single notation that uses the least powerful abstraction in order to translate sugared code into de-sugared code in the most flexible way possible. I will present a project I have been working on to implement computation expressions in Scala. In particular, I will show how this notation helps write asynchronous code with very little cognitive overhead.

Vlcsnap 2015 12 29 13h16m48s293 thumb
Rating: Everyone
Viewed 103 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

What happens when you take a 2011 CoffeeScript web app designed to edit 100,000-word novels...and scratch-rewrite it in Elm? It turns out the result is faster, more robust, and massively easier to maintain. Elm's simple design means that even a functional programming novice can quickly get up to speed on its static type inference, pervasive immutability, and first-class FRP system. It's not only an excellent language, but also a great introductory FP language that any JavaScript developer can pick up. This talk dives into the nuts and bolts of shipping a production web app in Elm, including questions like why you should choose Elm, how you transition from imperative architecture to FRP, and to what extent you can leverage the JavaScript library ecosystem without sacrificing your functional invariants. Come see how pleasant functional programming in the browser can be!

Vlcsnap 2015 12 29 13h14m14s277 thumb
Rating: Everyone
Viewed 71 times
Recorded at: May 22, 2015
Date Posted: December 31, 2015

Traditionally, in Computer Science, sets are assumed to be the basis of a type theory, together with Boolean logic. In this version of type theory, we do not need sets or Boolean logic; intuitionism is enough ("no principle of excluded middle required"). The underlying math is Topos Theory, but you are not required to be even aware of its existence. The theory is described using diagrams, not the traditional (and tricky) deduction rules. The resulting theory turns out to have dependent types. A simple "real-life" example or two will illustrate all this.

Vlcsnap 2015 12 29 14h30m52s177 thumb
Rating: Everyone
Viewed 76 times
Recorded at: May 22, 2015
Date Posted: December 31, 2015

This is the story of a road less traveled. In this talk we're going to take a look at the impact of choosing less common technologies like Scala and Clojure at an organizational level at Elemica. That will include some things that worked well for us, some things that didn't work so well, a myth or two we were able to dispell along the way, and land with why the process of figuring all of that out is a worthwhile endeavor.

Vlcsnap 2015 12 29 14h33m54s821 thumb
Rating: Everyone
Viewed 69 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

Birds travel thousands of miles each year to migrate, flying for hours on very little food and rest. By comparison, migrating databases seems like a paltry feat. Birdwave is a way to visualize the amazing phenomenon of bird migration. Using ClojureScript and Om allowed the app to be written in a declarative, concise manner, taking full advantage of JavaScript interoperability, as well as Clojure’s awesome built-in features such as persistent data structures and the async module. Also, prepare to be dazzled by the data-viz powerhouse that is d3. No birds were harmed in the creation of Birdwave. Or this talk.

Vlcsnap 2015 12 29 13h16m54s892 thumb
Rating: Everyone
Viewed 74 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

Do you enjoy Lisp-based languages, built on s-expressions and homoiconicity? Do you like writing syntactic abstractions with pattern matching? What if you could use a Lisp to write a fault-tolerant, highly-available distributed datastore? Welcome to the wonderful world of LFE (Lisp-Flavored Erlang)! I'll cover the basics of LFE, its toolchain, the macro system, and its intermediate representation step to Core Erlang, ending up on BEAM, the Erlang virtual machine.

Vlcsnap 2015 12 29 14h31m58s233 thumb
Rating: Everyone
Viewed 98 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

In this talk, I'll look at how design patterns from OOP translate to Clojure: some are unnecessary, some are embedded in the language, and others are easier to build.

Vlcsnap 2015 12 29 14h30m11s566 thumb
Rating: Everyone
Viewed 29 times
Recorded at: May 22, 2015
Date Posted: December 31, 2015

FP is often glibly described as "programming with functions", but we can equivalently say that FP is about programming with values. Functions are values, failures are values, effects are values, and indeed programs themselves can be treated as values. This talk explores some consequences of this idea of programs-as-values by looking at doobie, a pure-functional database library for Scala. We will examine the low-level implementation via free monads over algebras of the JDBC types, and show how this naturally enables an expressive and safe high-level API with familiar, lightweight, and composable abstractions including streaming result sets, and trivial compatibility with other pure libraries like Remotely and HTTP4s. Even if you are not in the market for a database layer, this talk will provide a practical outline for a general solution to dealing with terrible APIs (like JDBC) in a principled way.

Vlcsnap 2015 12 29 13h11m17s721 thumb
Rating: Everyone
Viewed 71 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

At the heart of intuitionistic type theory lies an intuitive semantics called the “meaning explanations." Crucially, when meaning explanations are taken as definitive for type theory, the core notion is no longer “proof” but “verification”. We’ll explore how type theories of this sort arise naturally as enrichments of logical theories with further judgements, and contrast this with modern proof-theoretic type theories which interpret the judgements and proofs of logics, not their propositions and verifications. Expect the following questions to be answered: What is the difference between a judgement and a proposition? What is a meaning explanation? What is the difference between a proof and a verification? The so-called semantical approach to type theory is, in the speaker's view, more immediately philosophically acceptable than the modern syntactic one, and also provides a basis for a future where partiality and other effects may be treated naturally through refinement and behavioral typing, rather than by means of term-level monads and similar kludges.

Vlcsnap 2015 12 29 14h35m06s976 thumb
Rating: Everyone
Viewed 92 times
Recorded at: May 22, 2015
Date Posted: December 30, 2015

React has popularized the idea of user interfaces as pure functions of application state, an approach which is perfectly suited for a language like PureScript. In this workshop, we'll learn how to use React and PureScript to create clean, well-factored web applications. This workshop assumes only basic knowledge of PureScript (or a related language such as Haskell), and for that reason, it can be considered a continuation of the earlier PureScript workshop for beginners.

Vlcsnap 2015 12 29 13h16m18s435 thumb
Rating: Everyone
Viewed 81 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

HTTP is a fascinating standard — one of those that we all use every day. But there are many different ways of reasoning about what HTTP "should" mean. We'll look at some of the approaches taken to model the HTTP layer, particularly in functional programming. Graphs, proofs, type systems — they're all fair game!

Vlcsnap 2015 12 29 14h29m32s609 thumb
Rating: Everyone
Viewed 74 times
Recorded at: May 22, 2015
Date Posted: December 31, 2015

Axle is a Scala-embedded domain-specific language built on Spire. This talk will cover the architecture and objectives of the project. Live coding examples will show how "design patterns" from Abstract Algebra apply to a range of domains including machine learning, bioinformatics, game theory, statistics, and data visualization.

Vlcsnap 2015 12 29 13h13m59s741 thumb
Rating: Everyone
Viewed 75 times
Recorded at: May 22, 2015
Date Posted: December 31, 2015

Emily is an experimental language project focusing on simplifying the basis of programming languages: it models all language operations through composition of function-like entities, equivalent to combinators with state. This means functions, objects, classes, and variable scopes have the same interface and are generally interchangeable. The goal is to make FP language capabilities accessible to entry-level and FP-wary programmers by means of simple concepts and a configurable, scripting-language-like syntax.

Vlcsnap 2015 12 29 13h16m04s487 thumb
Rating: Everyone
Viewed 50 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

Building computer systems that are reliable is hard. The functional programming community has invested a lot of time and energy into up-front-correctness guarantees: types and the like. Unfortunately, absolutely correct software is time-consuming to write and expensive as a result. Fault-tolerant systems achieve system-total reliability by accepting that sub-components will fail and planning for that failure as a first-class concern of the system. As companies embrace the wave of "as-a-service" architectures, failure of sub-systems become a more pressing concern. Using examples from heavy industry, aeronautics and telecom systems, this talk will explore how you can design for fault-tolerance and how functional programming techniques get us most of the way there.

Vlcsnap 2015 12 29 14h30m26s221 thumb
Rating: Everyone
Viewed 84 times
Recorded at: May 22, 2015
Date Posted: December 31, 2015

R&D on reactive programming is growing and this has delivered many language constructs, libraries and tools. Scala programmers can use threads, timers, actors, futures, promises, observables, the async construct, and others. Still it seems to us that the state of the art is not mature: reactive programming is relatively hard, and confidence in correct operation depends mainly on extensive testing. Better support for reasoning about correctness would be useful to address timing dependent issues. The Algebra of Communicating Processes (ACP) has a potential to improve this: it lets one concisely specify event handling and concurrency, and it facilitates reasoning about parallel systems. There is an ACP-based extension to Scala named SubScript. We show how it helps describing the internal behavior of Akka actors, and how it combines with futures. For more information see www.subscript-lang.org.

Vlcsnap 2015 12 29 13h11m04s609 thumb
Rating: Everyone
Viewed 92 times
Recorded at: May 22, 2015
Date Posted: January 4, 2016

John has no clue what the next great functional programming language will be like, but he's more than happy to hop up on stage and rant against type classes, nominative typing, data, modules, pattern matching, recursion, and, well, basically everything else you associate with functional programming! John will argue that to make radical progress in cheaply building correct software, we need to take one step backward and two steps forward, embracing dependent-typing, total functions, Turing-complete compilers, host languages, and automated proof search. Attend this talk to question your assumptions about functional programming... or just to heckle! Either way, all are welcome.