An Alien Lambda Calculus
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?
Outline/Structure of the Talk
In this talk I will first lay out the premise, mostly described in the abstract as it is, except in richer details. Specifically I'd like to consider a variant lambda calculus as being invented by beings of pure energy and live in shells of energy levels.
Throughout this, I will contrast and analogize this with the pure lambda calculus of Alonzo Church. I will nail down exactly which part of the pure lambda calculus is actually performing computation (spoiler: it's beta reduction). This is to be contrasted against the notion of computation previously described in the alternate universe.
I will then show that alpha conversion is somewhat destructive of information, and how preserving names might be a good thing. I show this in the context of compiling lambda calculus to von Neumann machines.
Last I will walk through a new lambda calculus that was recently invented that addresses the issues raised in the talk. I will suggest that this new lambda calculus might actually be a better lambda calculus in general.
Despite being slightly philosophical, I plan to actually show concrete results. At the time of writing this, I have the concrete results of the new lambda calculus. However, visualization of the alternate universe's lambda calculus is yet to be complete, but will hopefully be complete by Lambda Jam
Learning Outcome
By the end of the talk, I hope audience members will learn more about the notion of computation, and of lambda calculus.
Because this talk is slightly on the philosophical side of things, I also hope that audience members will walk away having a greater appreciation for the the simple good philosophical idea that syntax represents computation.
Last I want the audience members to take away that the new lambda calculus proposed is indeed a better one than Church's pure lambda calculus.
Target Audience
People interested in the foundations of functional programming. People interested in the very notion of computation.
Prerequisites for Attendees
Participants should be mildly familiar with lambda calculus. At least the notion of beta reduction should be known. It'll be introduced, but briefly.
Participants should also be mildly familiar with procedural programming written in C-style syntax.
Beginners are welcome, as no complex topics like types are introduced.
Links
Public Talks (in descending chronological order)
- Strange Loop 2018: A Funny Thing Happened on the Way to Reimplementing AlphaGo in Go
- GopherCon Singapore 2018: The Lost Art Of Bondage
- GopherCon Singapore 2017: Writing Efficient Multi Dimensional Slices
- PyCon 2015: Monads, In My Python?
My Blog (more interesting pieces linked below). An alternate blog for matters on computation
schedule Submitted 1 month ago
People who liked this proposal, also liked:
-
keyboard_arrow_downPhilip Wadler - (Programming Languages) in Agda = Programming (Languages in Agda)
Philip WadlerProfessor of Theoretical Computer ScienceUniversity of Edinburghschedule 2 months ago
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.
-
-
keyboard_arrow_downEdward Kmett / Tony Morris - Let's Lens
Edward KmettChair of the Haskell Core Libraries Committee, Software Engineering LeadSenior Software Engineer at Digital Asset
Tony MorrisSr. Software EngineerQueensland FP Lab, Data61schedule 2 months ago
480 Mins
Introductory Workshop
Beginner
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.
-
-
keyboard_arrow_down
Edward Kmett - Logic Programming à la Carte
Edward KmettChair of the Haskell Core Libraries Committee, Software Engineering LeadSenior Software Engineer at Digital Assetschedule 2 months ago
30 Mins
Invited 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. -
