Beyond functional programming: a taste of Verse. Simon Peyton Jones & Tim Sweeney | Lambda Days 2023
HTML-код
- Опубликовано: 8 сен 2024
- Keynote talk by Simon Peyton Jones and Tim Sweeney from Epic Games.
Verse is a new programming language, being designed at Epic Games as the language of the metaverse. Verse is a functional logic language, with a bunch of innovative ideas. Like Haskell, Verse is declarative (a variable in Verse stands for just one, immutable value), and higher order (lambdas are first class). But Verse goes well beyond Haskell, with existential variables, unification, expressions that yield multiple values, and much more besides. In this talk we'll give you a sense of what functional logic programming is about, what it looks like to program in Verse, and how we can give meaning to Verse programs using rewrite rules.
![[ICFP'23] The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programmi...](http://i.ytimg.com/vi/5P2pz1Xtjww/mqdefault.jpg)
![Run Away - Tzuyu(TWICE) ツウィ 쯔위 [Music Bank] | KBS WORLD TV 240906](http://i.ytimg.com/vi/KnHNNyAYiu0/mqdefault.jpg)
"Types are Values"! I have always waited for this. Let's start writing poems!
In Python you can assign types to a variable, just to note that this specific feature has been implemented before.
Tim Sweeney: "Actually we can solve the halting problem"
Simon: "NO no no no no we can't do that Tim that's impossible" (with a 'we talked about this' voice)
You can solve the halting problem for programs less than a K factor in size. Our computers actually don't have infinite amount of processing speed and memory, and our programmers only have a finite amount of brain power.
Well, yes ... but actually, in practice big theoretical barriers may turn out to be somewhat negotiable.
To take a classic example, the unification algorithm used for type inference and checking in Standard ML is exponential - NP-Hard or worse iirc: so compiling an ML codebase beyond a very restricted size should be impossible, shouldn't it?
...Or (demonstrably) not! As the authors of one notable early paper on the subject put it:
"Our worst-case lower bounds stand in contrast to practical experience, which suggests that commonly used algorithms for type reconstruction do not slow compilation substantially."
In practice, if your compiler's type inference algorithm (or, in this case, its partial program verifier) cannot process your code within a reasonable time (as determined primarily by your patience and expectations), then you just hit Ctrl-C and examine whether you can give it some extra hints (or perhaps restructure your code a little) to make its task easier. In the case of ML, this happens rather rarely (although it's quite easy to create pathological code if that is your deliberate aim).
Will such a fortuitously benign state of affairs be achievable for Verse's functional + logic hybrid?
That will depend partly on engineering, partly on some of the fundamental choices made in the design of the language (and perhaps a small dose of luck); it wouldn't be too surprising to find the fullest expression of MaxVerse containing features that can/will never be implemented but somehow anchor the cohesion of the implementable fragments of the language.
SPJ seems to think that it could work, and his previous hunches about such things have certainly often been on the money ... 😇
@@aoeu256 Solve the halting problem for the busy beaver algorithm for , say n=5.
I'm sure we'll know when it'll halt after a few billion years.
@@aoeu256 You can run a loop for every atom in the universe, technically.
Tim obviously meant that with proper constraints you can solve it. You just can't in the general case.
I have high hopes for actually being able to use something like this in the real world. If it winds up shipping with Unreal, I'll definitely switch over from Unity to have an opportunity to use it.
The tuple example of existential types is interesting. Very curious to see what it'll feel like in a full program. Thanks for the talk!
Millions of concurrent users, self-updatable, safe... I need to stop watching these Erlang videos.
That’s a great talk, and it’s interesting to see which new concepts in PL design such research will open.
@42:30
Is the declaration:
fst(p:tuple(int, int)):int := x:int; y:int; p = (x, y); x
equivalent to:
fst(p:tuple(int, int)):int := let x; let y; p = (x, y); x
Hoping for a single language that's acceptable (maybe even likeable) by
the Java, Haskell, Lisp, Elixir, ML, Scala, & Prolog people.
Could Verse be the Next Big Language (NBL) ?
What I don't get, you get this living legend to give a talk, but this tiny timeslot. He clearly wants to tell way more, like what was so important that came after him?
Love it!!!!!!!!!!!!!!!!!!
Is it open source yet? Is there a dummy repo to follow?
Gnarly
Absolutely love it!!!!!
Sign me up, where do you need me at to help pitch in. This is the next best thing since HyperMac and ExperLisp. So im sql rpn strictly typed dynamicly functional and a totally artificially intelligent programmer!!
:-)
Somehow I actually kind of like it.
Tim Sweeney: "I want the language to be easy to learn so I can get tons of developers to make free content for my company and make it really easy for me to exploit them."
Also Tim Sweeny: "This new language is Haskell but if it was Prolog and required a university-level maths education in formal logic to understand, and also I got one of the Haskell guys to help make it (Haskell being a language that's incredibly easy to pick up and used by absolutely everyone in the games industry), and also I'm making vague promises about distributed systems that absolutely anyone who has interacted with a database in the past few years knows are complete and utter bullshit."
This is such a comical talk, I don't understand how people didn't burst out laughing during it.
I'm not finished with the video yet, but it doesn't look like it has any of the hard stuff from Haskell. Unless it goes off the rails, it does seem like a simple enough language to pick up.
The core of haskell is easy to learn [for example there are high-school studies where they taught high school students to make games in haskell], but when you start going into the category theory terminology and making applications that run quickly and writing your program so that it can do what Lisp or Python does with their macros and monkey patching and global state and have it test for your errors at compile time and actually understand the error messages then yeah Haskell is hard.
@@2Cerealbox It literally has 'abilities' from Unison in it. They're like monads but only slightly easier to understand. In addition, it takes everything you know about pure functional programming and throws it out the window because now it uses _logical_ programming instead. Which ok cool, but there are lots of limitations to that and it's **definitely** not easiest for beginners to pick up.
@samwright Abilities are pretty easy to understand
You nailed it. It's basically pure functional programming at the end of the day still, and this is a paradigm many find difficult.
Cool stuff
logic programming for the masses, what a great language which I'll never use
doh! you misheard or misunderstood.
it's called _functional _*_logic_* programming:
a superset of function programming & with aspects of logic programming.
different than any other platform you know, except for you know, the web
I don’t understand how this can be presented in this way by, and to, people that have had enough exposure to Prolog.
🔥
is that fucking comic sans?
When you break 1 billion you choose the font you want
SPJ always uses comic sans.
In fairness Tim made him isolate it into a separate slide-pack that he had to alt-tab to.
SPJ is an exulted being and can use whatever font he wishes.
1:06:00 I'm not typing Cyrillic.
its not cyrillic and thats not code. its math notation.
lmao metaverse
Also listening to Tim Sweeney try to mansplain logical programming to a group of mathematics and functional programming nerds who all took Prolog in university is so fucking funny lmaoooo
It's literally a lecture
Its a lecture dude.
lmaoooo at your pointless life 🤣😆🤣😆🤣
Kind of sounds like an uninspired Go.
youve not understood what theyre doing, then. its nothing at all lie Go, and its far from uninspired.
little minds
are blind to
paradigm shifts
Lmaoo i mean there's plenty to critize, but definitly not, that they're afraid to go against the norm. Also have you ever written a single line of go? Lol