- Getting close to the conceptual metal: Lambda calculus and Scott encoding
The Lambda calculus is a universal model of computation, and Scott encoding is a method of representing any algebraic data type within it. If that sounds interesting, come, share a buffer as we see how much we can build using nothing but hot air.
- Hack Night Feb 2020
BFPG Hack Night returns! Come along and hack on whatever you want. Ask questions. Join a project. Do some coursework / workshop exercises. Share your ideas, discoveries, frustrations, projects. We are likely to go somewhere for eats/drinks after 20:00+10:00. Hard limit of 12 people. (We'll find another place for future events if we keep maxing out The Edge.)
- BFPG Monthly Meetup (Please read description! :))
Introduction to ADTs and Reasoning about the Cardinality of Types - Jack Kelly Abstract TBD For part two, I'd like to not have a talk and instead have an open discussion with the whole group about why they are interested in FP, what they have learned recently and what they are stuck on. We'll kick things off with Matt Peddie and myself briefly talking about how we harness FP at our respective works and the interesting parts that make FP deliver value to their work. I don't really know how it'll pan out in reality, but my goal for the session is to get a good feel for where everyone is at and what they are interested in and create some networking opportunities for new people and new ideas to connect. I feel personally disconnected from everyone's journey at the moment and feel like I at least need to reconnect with that to be a good organiser. With the common patterns that come up from the discussion, we can then create a queue of BFPG talks to help fill the gaps and satisfy the interests people have. To give y'all some renewed opportunity to participate and shape BFPG to your own needs rather than just listening to whatever talk is on. So please come loaded with a list of things that you have found cool or particularly puzzling and we'll see what happens. If you want to show off some code on a laptop, just make sure that it can talk HDMI and rock up before 1745 so we can pretest AV. :) The plan would be to have Jack's talk, pizza break then use the remainder of the time to have this chat. If you think that this idea sucks or could be tweaked a little let me know in comments or directly to [masked]. It's only worth doing if you feel like it's worth your time. --- As a backup I can talk at a very high level about the pieces of a really awesome power to safety weight ratio function that I wrote recently. But if I'm going to do that I need a bit of lead time so please let me know if you want that instead early, lol. :) https://gist.github.com/benkolera/d0ee177b531925fbc5ec7a5a83b0e8c8
- BFPG Monthly Meetup
Introduction to Currying - Jack Kelly -------------------------------------------------- New functional programmers are often taught "this is how you write a two-argument function": sum : Int -> Int -> Int sum x y = x + y In Elm and Haskell, there is actually no such thing as a "two-argument function". All functions take only one argument, and "multiple arguments" are handled via Currying (i.e., with functions that return functions). This talk will look closely at some Curried functions from the built-in libraries, in order to unlock new perspectives on familiar functions. It is aimed at beginners, but intermediate functional programmers should gain something as well. Examples will be in Elm where possible, and Haskell where necessary. Practical Examples of writing programs and proving theorems in Idris - Donovan Crichton ---------------------------------------------------------------------- Writing programs and proving theorems can be the same thing! In this talk we'll show you exactly how the Curry-Howard isomorphism applies in Idris, by covering the following topics: *A brief intro to logic (propositional and first-order). *A brief intro to dependent types. *A demonstration of proving basic theorems in Idris. *A comparison of theorem proving vs actually programming. *A real-world example of discharging proof obligations while using Idris. -------------------------------------------------------------------------------- Handy Prerequisites: ------------ It would help if attendees are: *Comfortable with Haskell syntax for types and functions. *Aware of the Haskell syntax for GADTS (Generalised Algebraic Data Types) *Rusty with the notions of propositional and first-order logic. *Aware of dependent types.
- Brisbane Tech Drinks
- Haskell Type Level Programming + Servant - Jack Kelly & Brad Parker
There will be a pair of matched talks at BFPG this month: First up, Jack will give us a tour of Haskell's type-level features and some smaller motivating examples showing how they work. After pizza, Brad will look at how the Servant library uses these type-level features to turn a type-level description of an API into servers, clients and other targets.
- haskell.nix by Hamish Mackenzie & Intuition for Propagators by George Wilson
haskell.nix - an alternative infrastructure for building haskell packages - Hamish Mackenzie (Visiting from NZ!) haskell.nix provides a nix build infrastructure for haskell packages and projects. The primary use case for haskell.nix is to serve as the substrate to build any haskell project in CI without having to resort to modifications to the project. haskell.nix has support for cabal projects as well as stack projects. It features component level build granularity and very good support for cross compilation. iohk uses nix in production and the whole ci pipeline is setup using nix and hydra. We do however need to produce build products for windows, for which nix does not exists and which is a pain to deal with. This lead us to investigate cross compilation of haskell packages to windows. After we ran into numerous issues with the current haskell build infrastructure in nix, and especially the cabal2nix tool. Another issue we've run into was performance. After trying to amend the existing haskell infrastructure, we saw that our changes were non-trivial and would not be easy to reconcile with upstream without breaking every existing setup. This lead to haskell.nix, which focuses on performance, cross compilation, supporting cabal and stack projects as well as ease of use. https://github.com/input-output-hk/haskell.nix ---- An Intuition for Propagators - George Wilson The propagator model of computation developed by Radul and Sussman consists of stateful cells connected by independent stateless machines called propagators. These propagator networks are a helpful way to structure or think about computations, particularly those that are concurrent or distributed. This talk will give an intuition for what these propagator networks look like, why they work, and how we can use them to build programs. Efficient implementation will not be covered. The Haskell community has recently seen concurrency abstractions bearing similarities to propagators, such as the work on LVars by Kuper and Newton; and also projects directly influenced by propagators, such as Edward Kmett's recent work. ---- Reflex Outside the Browser - Jack Kelly Functional Reactive Programming (FRP) is often introduced by discussing events and behaviors, and how to transform and mix them. But once you understand the primitives, what do you do with them? Where do the first events come from, and how do you wire these parts into a larger whole? FRP promises benefits in more domains than just user interfaces, so let's take a look at Reflex outside its most common habitat of web frontends. There's now a fairly up-to-date version of Reflex on Hackage, so we can play with it right away and leave GHCjs, Reflex-DOM, special build tools, and the custom nix frameworks for later. An FRP network of events and behaviors runs inside a library called a "host", which interfaces between the FRP network and the outside world. Using an interactive OpenGL program as our example, we'll explore how a slightly larger reactive program hangs together, and how it uses the host's features to do what it needs to do.