Can all functions in Haskell be represented using the lambda calculus?

I’m learning Haskell from the textbook Haskell Programming from First Principles. I’m two chapters in, and I want to write about what I’ve learned.

I want to start by first introducing the concept of a function and then introducing the concept of the lambda calculus. Is it accurate for me to connect the two concepts by saying, “All functions in Haskell can be represented using the lambda calculus”?

Welcome here @filenine

I would be a little cautious before dashing into print. Haskell rests on lambda calculus, yes. But also on Algebraic DataTypes. So I’d put it that at the First Principles level “All functions in Haskell can be represented using the lambda calculus plus pattern matching on ADTs.”

(At a deeper level pattern matching also can be explained in terms of lambda calculus, but that’s not how it’s represented nor how it’s implemented in Haskell.)

It would be more accurate to say that functions in Haskell can be represented with a lambda calculus, and which particular one depends on which Haskell you mean. The Gitlab wiki page on System FC has some interesting background.

Thank you both for taking the time to answer my question.

True. I’m not trying to write a reference text; it’s more a collection of the notes I’m making when going through the book. I want to structure them in a readable way so I can use them later and possibly show them to other people.
This is my first time learning functional programming and theoretical programming language concepts, so I haven’t learned about the concept of algebraic data types yet. Once I learn about them, I’ll bring them up in my notes.

There’s more than one Haskell? I thought there was a single Haskell programming language.

1 Like

Errrmmm. Something you’ll have to suffer in the Haskell community is there’s no such thing as a simple question, let alone a simple answer. Somebody will immediately want to complexify the whole business.

It’s ok, just roll with it: I’ve never seen that wiki page before, and I’ve been happily using Haskell for over a decade. Yes you’ll have to get to know the agonies of System FC in due course; but not at the “First Principles” stage.

And shame on @jhenahan for linking to a page that’s " out of date (as of July 2019)". To pick some nits: it’s not that there’s more than one Haskell. It’s not even that there’s more than one lambda calculus. Rather, there’s more than one way to give a semantics for lambda calculus; a learner will get some glimmerings of those ways when they advance to partial applications and overloading (type classes) and type unification.

3 Likes

You can use Scott encoding to embed ADTs in a lambda calculus, pattern matching is just a much nicer syntax. :slight_smile:

A more difficult sticking point is type classes, though if you translate constraints to normal arguments and do explicit dictionary passing, you can encode them in a lambda calculus.

A simply typed lambda calculus doesn’t have parametric polymorphism, so that won’t work. You could erase all the types to use a untyped lambda calculus, but the report mostly tells you how to lower to a polymorphic lambda calculus sans explicit type binders (no syntax for higher-rank types) and primitive pattern matching (only on outermost constructor; rather than going all the way to Scott encoding).

(Haskell as extended by) GHC needs polymorphic lambda calculus with explicit type binders (for higher-rank types) and some sort of (primitive?) Leibniz equality type/value to implement type equality constraints for GADTs (at least).

But, given that untyped lambda calculus is computationally equivalent to Turing machines, you can reduce any language to lambda calculus if you work hard enough at it. :stuck_out_tongue:

2 Likes

A quite easy to read introduction (of lambda calculus itself too) is SimonPeyton Jones et al.: The Implementation of Functional Programming Languages - just substitute Miranda with Haskell. As it’s from 1987, it isn’t up-to-date, but it’s great to understand the basics:
PDF

I enjoy the complexifying — it shows me that the language is deeper than I can currently imagine.

That said, I think the answers I’ve been given have assumed that I know a lot more about programming language theory than I actually do. I’m a computer science undergraduate student. Haskell is the first functional language I’m learning, and I’m learning it because I think it’s interesting.

I have a friend who does something along those lines — he’s studying formal program verification, and he verifies processes by reducing the languages they’re written in to their basic elements.

I’m going through this book; so far, it seems well-written and all the topics it covers have been explained clearly. Thank you for sharing it with me.