addressalign-toparrow-leftarrow-rightbackbellblockcalendarcameraccwcheckchevron-downchevron-leftchevron-rightchevron-small-downchevron-small-leftchevron-small-rightchevron-small-upchevron-upcircle-with-checkcircle-with-crosscircle-with-pluscrossdots-three-verticaleditemptyheartexporteye-with-lineeyefacebookfolderfullheartglobegmailgooglegroupshelp-with-circleimageimagesinstagramlinklocation-pinm-swarmSearchmailmessagesminusmoremuplabelShape 3 + Rectangle 1ShapeoutlookpersonJoin Group on CardStartprice-ribbonShapeShapeShapeShapeImported LayersImported LayersImported Layersshieldstartickettrashtriangle-downtriangle-uptwitteruserwarningyahoo

Types Are Theorems; Programs Are Proofs

  • Jul 14, 2014 · 6:30 PM

Join Philly Lambda and speaker Mark Jason Dominus for another talk diving into the deep waters of type theory and the Curry-Howard correspondence.  Mark writes:

One of the most famous features of functional languages such as Haskell and Scala is their complex, fine-grained type systems. In Haskell, we find that it's easy to construct functions with types

a -> (b -> b)
a -> (b -> a)
a -> (a -> b) -> b

but it is impossible to construct functions with types

a -> (a -> b)
(a -> b) -> a
(a -> b) -> b

What is the distinction here? The answer is astounding:

There is a function of type T if and only if T, reinterpreted as a statement of logic, is a *true* statement.

The correspondence goes futher: if you have a program P with type T, then not only can you understand T as a theorem of logic, but you can understand P as a proof of the theorem. Or working the other way, if you have a proof P of some logical theorem T, you can convert P into a program whose type is T.

This is the foundation for more complex, dependently-typed languages such as Agda where the type of a program P are understood explicitly as assertions about the behavior of P.

Join or login to comment.

  • Tim V.

    Monday's are out for me. Really wish I could make it. :( Any chance of a recording?

    July 2, 2014

  • Mark D.

    Thanks for coming to my talk yesterday! I hope everyone had a good time. The complete slides (including the ones I didn't get to about logical-or and negation( are at . Please feel free to email me with questions at [masked].

    2 · July 15, 2014

  • Jim

    Mark, thanks for the great talk! Got me excited about learning some agda!

    2 · July 15, 2014

  • A former member
    A former member

    What floor is SevOne at? I do not see it on the board...

    July 14, 2014

    • A former member
      A former member

      Never mind... it is the 11th floor

      July 14, 2014

  • Michael R.

    Is the presentation starting at 6:30, or is that just the arrival time?

    July 14, 2014

    • Dan M.

      good question. i guess it depends when mark and or the pizza get here.

      July 14, 2014

  • Daniel M.

    Sorry, something has come up, I can't make it out tonight.

    July 14, 2014

  • Paul S.

    We've had to move the date of this talk from Wednesday, July 9 to Monday, July 14. Apologies for the inconvenience.

    July 1, 2014

20 went

Our Sponsors

People in this
Meetup are also in:

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy