Home

The Verse Calculus: a Core Calculus for Functional Logic Programming

The Verse Calculus: a Core Calculus for Functional Logic Programming

https://simon.peytonjones.org/assets/pdfs/verse-conf.pdf

  • LENNART AUGUSTSSON, Epic Games, Sweden
  • JOACHIM BREITNER
  • KOEN CLAESSEN, Epic Games, Sweden
  • RANJIT JHALA, Epic Games, USA
  • SIMON PEYTON JONES, Epic Games, United Kingdom
  • OLIN SHIVERS, Epic Games, USA/li>
  • TIM SWEENEY, Epic Games, USA

Functional logic languages have a rich literature, but it is tricky to give them a satisfying semantics. In this
paper we describe the Verse calculus, VC, a new core calculus for functional logical programming. Our main
contribution is to equip VC with a small-step rewrite semantics, so that we can reason about a VC program
in the same way as one does with lambda calculus; that is, by applying successive rewrites to it.


This draft paper describes our current thinking about Verse. It is very much a work in progress, not a finished
product. The broad outlines of the design are stable. However, the details of the rewrite rules may well change; we
think that the current rules are not confluent, in tiresome ways. (If you are knowledgeable about confluence proofs,
please talk to us!)We are eager to enagage in a dialogue with the community. Please do write to us.

By cdiggins at 2022-12-12 16:23 | Functional | other blogs | 18125 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Also see the slide deck

Also see the slide deck Beyond Functional Programming: The Verse Programming Language.

View from 100,000 Feet
  • Verse is a functional logic language (like Curry or Mercury).
  • Verse is a declarative language: a variable names a single
    value, not a cell whose value changes over time.
  • Verse is lenient but not strict:
    • Like strict:, everything gets evaluated in the end
    • Like lazy: functions can be called before the argument has a value
  • Verse has an unusual static type system: types are firstclass values.
  • Verse has an effect system, rather than using monads.
By cdiggins at Mon, 2022-12-12 16:37 | login or register to post comments

Interesting

The world may know Tim Sweeney for other things, but personally I will always know him as LtU user 97.

Seriously, that's a real co-author hall of fame...

By Matt Hellige at Tue, 2022-12-13 00:09 | login or register to post comments

Also published in ICFP

This has also been publish in Proceedings of the ACM on Programming Languages,Volume 7,Issue ICFP as The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming

By jrincayc at Tue, 2023-12-12 02:13 | login or register to post comments

Video Presentation

Here is a video presentation by SPJ and Sweeney:

Beyond functional programming: a taste of Verse. Simon Peyton Jones & Tim Sweeney | Lambda Days 2023

By mlhaufe at Thu, 2024-01-11 00:12 | login or register to post comments