While you were talking about Verse, I had trouble understanding why Epic Games would choose to do a functional logic programming language for scripting for Fortnite and UE. But then SPJ said that Tim Sweeney is a geek who has been thinking about it for two decades and is convinced that this is the best way to write software - and it all made sense!
Well, Tim is a programmer first and foremost before becoming a CEO, unlike the new wave of tech CEOs whos backgrounds are business, marketing or other no techy majors. He is one of the OG ones where only geeks would be interested in the tech field.
In addition to the other comment, consider the target use for verse by Epic itself. Game engines (or indeed whatever you do with UE these days) often suffer from imperative constraints in ways than less complex structures do not. This is most game logic is at least contextually single threaded, which has additional performance issues. I think that for Sweeney this works out to something that satisfies his engineering itch, while also experimentally approaches addressing real design problems.
Likewise! I've been browsing youtube for months wondering what I was missing out on. And then I stumbled on this and I've just binged it every day at work.
I wanna thank you Kris, as a compiler nerd, for all the beautiful conversations you share with us, the best Simon Peyton Jones and, recently, Chris Lattner, both of these interviews are worth rewatching.
For anyone who wants to implement a functional language, just follow SPJs book "Implementing Functional Languages" (including chapters by some other legends of CS). It basically is a step by step tutorial on how to implement Miranda/Haskell. It's truly a landmark book. That book and the paper "Practical type inference for arbitrary-rank types" it's pretty much "all you need" for designing and implementing advanced functional languages.
Simon is brilliant and he really loves what he does, he is truly admirable! I discovered your channel recently and I'm so glad I did, I've always missed in-depth programming content on RUclips.
Fantastic interview. Love to hear SPJ talk about anything, but I especially love hearing about Verse! It's a bit surreal hearing SPJ talk about Fortnite, but as Kris says at the beginning, Verse is a trojan horse. Exposing the practicality and beauty of functional programming to thousands of kids and gamers. Love it! ❤
Very interesting! And perfect timing! I've recently begun exploring functional programming with OCaml, and I really love the functional paradigm and the thought process of functional programmers. For me it's very concrete and easy to grasp. Being on the low end of an intermediate programmer, I think this is also why a lot of people start to learn programming but never stick with it. They probably saw a Python tutorial and so started to learn Python OOP, when their thought process and comfort could be more aligned with the functional paradigm. That's why I always encourage new programmers to take a survey of languages course to find what language and paradigm best suits them.
Functional programming clicks with me, but I'll keep learning C because of what I'm interested in doing. I always read that C is beautiful but that is not how it felt to me right from the beginning.
@@delibellus It certainly depends on what you're trying to do. C is the very first language I started with and learned, although I'm definitely no expert. I would say people who start with C or a similar lower-level language understand programming much better than people who start with very abstracted, garbage-collected languages.
Enthralling subject matter. At the risk of boiling it down to the point of losing some nutrients, the idea of extending a type system from "o is T" to "o satisfies a functionally determined contract T" is super powerful. Simon is a great speaker, and makes theory feel like an exciting frontier. I didn't have any interest in Verse before, but now I'm looking forward to a chance to try it, whether in Unreal or standalone. Thanks for both of your time and thoughts!
I've been greatly enjoying the interviews, Kris! You ask good questions and give space for guests to answer them. This was an especially fun interview to watch.
Truly some of the most insightful and thoughtful computing content on RUclips. Far prefer this over the other channels with many subscribers who don’t do much aside from reading through online articles.
I'm only halfway through the video, and obviously very excited with the subject and the guest, but wanted to point out that I really admire the host as well! Very pleasant and somehow refreshing language, gonna check out more videos definitely! High quality stuff
This Verse thing sounds super interesting. From what I gathered, it sounds like you keep adding "asserts/constraints" to a structure until you narrow down the level of "uniqueness" from the solution you want. This whole logical programing (functional or not) is something I've only heard about, but now I really want to actually try it out myself.
What a timing :d Very excited to listen to this, recently started getting more and more into FP (haskell), currently using it mostly for CLI/TUI apps :)
First of all, love the channel! I was looking for content like this and thank the celestial rewrite rules that I found it. Second, I have a basic question about functional logic programming to anyone who has the answer. In functional programming, our basic abstraction and means of computation is function application. We know how that can be done as there is plenty of literature on mapping the work of Church and Curry to the world of building functional compilers and interpreters (or just look up how apply+eval works in Lisps :) ). But in the world of functional logic programming, instead of N-ary functions, we have N+1-ary relations, and say I define the relational version of the map function (in a miniKanren-like syntax, modified a bit to decreate "jargon" for legibility): (define-relation map° [f xs ys] (disjunction (conjunction (== xs empty-list) (== ys empty-list)) (conjunction (exist [x xs' y ys'] (cons° x xs' xs) (apply° f [x] y) (cons° y ys' ys) (map° f xs' ys'))))) Looks like a straightforward translation of something like the naive Haskell version of map. But the key thing here is apply°, the relational equivalent of function application. My big problem is that I cannot imagine how to implement apply°. Any implementation I try to come up with, I just cannot find a proper algebra for treating f as the proper logic variable that can be passed around like this (hence the "higher order" phrase I keep using) and would work properly with unification in its environment and would also lead to values evaluated like a regular function would (again, tying back to unification). In addition to this, I don't even know if apply° should be implemented at this level, or at the constraint level (but that doesn't seem constructive on the face of it, as arbitrary function application very much does not seem like a finite domain). In a similar vein, how is an anonymous relation defined and implemented? I wonder how Verse implements this and if anyone can point me to literature where I might find the solution to this. I must admit I feel a bit like a fool, but my computer science background is quite limited in this area.
I love Prolog and recently finally learned CLP, but I’ve never found an excuse to dig into functional-logic programming. It seems like all his logic programming examples are all better solved by CLP(FD). Wow, he just mentioned Icon which was my favorite language back in the 90s.
I know of three logic programming languages: Prolog, Icon, and jq. jq is also a functional programming language, arguably, though jq is a bit of a toy (though a very useful toy!). To me Verse sounds like it shares a lot with Icon and jq: pervasive generators and backtracking, any values as truth / failure as falseness (in Icon in particular).
I am thinking of Alan Perlis' Quote "LIPS programmer know the value of everything and cost of nothing". If you abstract away execution details, you are making a tradeoff that makes the programmer's life easier when those details can be ignored, while making the programmer's life much harder when they can not be ignored. I find this to be pretty prounouced in Prolog where the language encourages the programmer to only state what they want, when in practice, the programmer has to think about the process that will ensue from the request, and when there is a disonnace between the way the programmer think and what they write, things become messy. If you are going to abstract away something from me, you better be sure that you can deal with the details yourself.
50:34 Isn't what Simon is describing just a dependent type of sorts? You have properties/predicates that you want and can define a type that includes only objects that have this property. (Fortnite should probably use Agda instead /s)
Almost. Part of the inspiration is a system called "Ontic," which originated the "single semantic category for types and terms" in the sense Verse uses, and also Jason Hickey's work on "Very Dependent Types." One difference is that Verse's type system doesn't make the "closed world" assumption. That is, it can't make global consistency claims. It can only say something like "given all the code I have access to, at least IT is consistent."
@@pooroldnostradamus Right. The most common (at least in type theory terms...) way to put it is there are two interpretations of "types," "Church types" and "Curry types." In the Church view, types define the semantics of the program: no types, no meaning. In the Curry view, an untyped program may very well have a meaning, and when you type that program, we hope and expect that the types reflect that meaning. When you stop and think about it, though, the Church view is unrealistic in a distributed setting: you can't know whether the "whole program" typechecks, because YOU don't have the "whole program," and in fact the "whole program" will change over time. So the Curry view it is! Now the wrinkle is that it's still the case that you don't have the "whole program." New bits will come and go; your own code will change in ways relevant to the types, etc. So all you can say in a distributed system from the Curry view is that, at any given moment in time, the (distributed) "program" you DO know about is consistent (in the logical sense implied by the Curry-Howard correspondence). The Verse verifier will provide "verification" in that sense.
If you have a line to Simon, I would be interested to know if there exists a version of CAS here in New Zealand. That part of the talk really resonated with me.
1:09:00 what a great talk on the perspective of how to better teach computer science and make it concrete. reminds of the white papers i've been reading play and education in general. you should get jonathan blow on to talk about jai and games for education.
I havent finished this video yet but im not sure i get the appeal/motivation for the functional logic programming. Isnt that what we already do, write functions with names that abstract the algorithm and return a result such that we dont have to understand the algorithm to use the function re. Example of x**2?
There was an interesting point about not being able to see the "what" immediately of an imperative program, i.e. to identify that a square root program is trying to compute the square root, whereas in a declarative program its the starting point, so you can just read it. But couldn't you equally say that in a declarative program, the "how" is not immediately obvious, and perhaps even hidden from you, whereas in an imperative program, its the starting point, so you can just read it...
ruclips.net/video/UBgam9XUHs0/видео.html Regarding "types" and verification: I wonder if SPT kept up with testing in Haskell, like quickCheck and property-based testing in general. And I wonder if SPT and Sweeney have thought about categories and homotopy. I'm sure he must have encountered "Computational Trinitarian" thought over the years... Thanks again for the great interview.
Soo this whole buzz on verse is based on a feeling and "tim was always right" (he wasn't but whatever ) Yikes. It tries to solve no problem, just force a lot of people to deal with it because it's "cool"
Yes of course, if we expect that we are writing some kind of functional assembly language or some bs... Functional languages still have compilers, they can produce low-level instructions no better or worse than any high-level imperative language for similar algorithms.
While you were talking about Verse, I had trouble understanding why Epic Games would choose to do a functional logic programming language for scripting for Fortnite and UE. But then SPJ said that Tim Sweeney is a geek who has been thinking about it for two decades and is convinced that this is the best way to write software - and it all made sense!
Well, Tim is a programmer first and foremost before becoming a CEO, unlike the new wave of tech CEOs whos backgrounds are business, marketing or other no techy majors.
He is one of the OG ones where only geeks would be interested in the tech field.
In addition to the other comment, consider the target use for verse by Epic itself. Game engines (or indeed whatever you do with UE these days) often suffer from imperative constraints in ways than less complex structures do not. This is most game logic is at least contextually single threaded, which has additional performance issues.
I think that for Sweeney this works out to something that satisfies his engineering itch, while also experimentally approaches addressing real design problems.
Why? Because it's better
@@maxrinehart4177why do you guys always need to insult. Being interested in the greatest invention known to man isn't "geeky".
This quickly became one of my favourite tech podcasts. It's crazy how much these videos align with my interests.
+100
Yes, rare find, and I binge all these :)
Likewise! I've been browsing youtube for months wondering what I was missing out on. And then I stumbled on this and I've just binged it every day at work.
it's the man himself! thank you Kris ❤️
The phrase "living legend" definitely applies. 👑😁
@@DeveloperVoices now get John Carmack!
I wanna thank you Kris, as a compiler nerd, for all the beautiful conversations you share with us, the best Simon Peyton Jones and, recently, Chris Lattner, both of these interviews are worth rewatching.
For anyone who wants to implement a functional language, just follow SPJs book "Implementing Functional Languages" (including chapters by some other legends of CS). It basically is a step by step tutorial on how to implement Miranda/Haskell. It's truly a landmark book. That book and the paper "Practical type inference for arbitrary-rank types" it's pretty much "all you need" for designing and implementing advanced functional languages.
Simon is brilliant and he really loves what he does, he is truly admirable!
I discovered your channel recently and I'm so glad I did, I've always missed in-depth programming content on RUclips.
Fantastic interview. Love to hear SPJ talk about anything, but I especially love hearing about Verse! It's a bit surreal hearing SPJ talk about Fortnite, but as Kris says at the beginning, Verse is a trojan horse. Exposing the practicality and beauty of functional programming to thousands of kids and gamers. Love it! ❤
Very interesting! And perfect timing! I've recently begun exploring functional programming with OCaml, and I really love the functional paradigm and the thought process of functional programmers. For me it's very concrete and easy to grasp. Being on the low end of an intermediate programmer, I think this is also why a lot of people start to learn programming but never stick with it. They probably saw a Python tutorial and so started to learn Python OOP, when their thought process and comfort could be more aligned with the functional paradigm. That's why I always encourage new programmers to take a survey of languages course to find what language and paradigm best suits them.
Functional programming clicks with me, but I'll keep learning C because of what I'm interested in doing. I always read that C is beautiful but that is not how it felt to me right from the beginning.
@@delibellus It certainly depends on what you're trying to do. C is the very first language I started with and learned, although I'm definitely no expert. I would say people who start with C or a similar lower-level language understand programming much better than people who start with very abstracted, garbage-collected languages.
Cant commend this channel enough. Absolutely great work, lovely guests, lovely host. Also love your nails Kris
Thanks! On both fronts! 😁
Enthralling subject matter. At the risk of boiling it down to the point of losing some nutrients, the idea of extending a type system from "o is T" to "o satisfies a functionally determined contract T" is super powerful. Simon is a great speaker, and makes theory feel like an exciting frontier. I didn't have any interest in Verse before, but now I'm looking forward to a chance to try it, whether in Unreal or standalone. Thanks for both of your time and thoughts!
I've been greatly enjoying the interviews, Kris! You ask good questions and give space for guests to answer them. This was an especially fun interview to watch.
Thanks George! That one was a particular pleasure to record - Simon's an absolute legend. 🤩
Truly some of the most insightful and thoughtful computing content on RUclips. Far prefer this over the other channels with many subscribers who don’t do much aside from reading through online articles.
I'm only halfway through the video, and obviously very excited with the subject and the guest, but wanted to point out that I really admire the host as well! Very pleasant and somehow refreshing language, gonna check out more videos definitely! High quality stuff
Thank you. SPJ's an absolute legend. If I can stand next to him and look even half-decent, I'm winning. 😁
This Verse thing sounds super interesting. From what I gathered, it sounds like you keep adding "asserts/constraints" to a structure until you narrow down the level of "uniqueness" from the solution you want.
This whole logical programing (functional or not) is something I've only heard about, but now I really want to actually try it out myself.
Wow, this is an amazing channel. Amazing interview. Thank you!
Its always enlightening to listen to SPJ. Thanks for making this happen Kris 🧡
Truly a great interview. Thank you!
What a timing :d
Very excited to listen to this, recently started getting more and more into FP (haskell), currently using it mostly for CLI/TUI apps :)
Simon just seems like such a nice and genuine person. Awesome stuff!
He really is. ❤️
im not quite done watching this but I have been having a good time watching. Good work!
Yay! That's really cool that there is language backed not only be researches. Those Curry, Mercurry, Ciao Prolog doesn't seem to have enough steam.
First of all, love the channel! I was looking for content like this and thank the celestial rewrite rules that I found it.
Second, I have a basic question about functional logic programming to anyone who has the answer.
In functional programming, our basic abstraction and means of computation is function application. We know how that can be done as there is plenty of literature on mapping the work of Church and Curry to the world of building functional compilers and interpreters (or just look up how apply+eval works in Lisps :) ).
But in the world of functional logic programming, instead of N-ary functions, we have N+1-ary relations, and say I define the relational version of the map function (in a miniKanren-like syntax, modified a bit to decreate "jargon" for legibility):
(define-relation map° [f xs ys]
(disjunction
(conjunction
(== xs empty-list)
(== ys empty-list))
(conjunction
(exist [x xs' y ys']
(cons° x xs' xs)
(apply° f [x] y)
(cons° y ys' ys)
(map° f xs' ys')))))
Looks like a straightforward translation of something like the naive Haskell version of map. But the key thing here is apply°, the relational equivalent of function application. My big problem is that I cannot imagine how to implement apply°. Any implementation I try to come up with, I just cannot find a proper algebra for treating f as the proper logic variable that can be passed around like this (hence the "higher order" phrase I keep using) and would work properly with unification in its environment and would also lead to values evaluated like a regular function would (again, tying back to unification).
In addition to this, I don't even know if apply° should be implemented at this level, or at the constraint level (but that doesn't seem constructive on the face of it, as arbitrary function application very much does not seem like a finite domain). In a similar vein, how is an anonymous relation defined and implemented?
I wonder how Verse implements this and if anyone can point me to literature where I might find the solution to this. I must admit I feel a bit like a fool, but my computer science background is quite limited in this area.
I love Prolog and recently finally learned CLP, but I’ve never found an excuse to dig into functional-logic programming. It seems like all his logic programming examples are all better solved by CLP(FD).
Wow, he just mentioned Icon which was my favorite language back in the 90s.
What an amazing channel !!! ❤❤❤
I'm so glad I found this awesome channel! Very cool stuff guests and a wide range of topics
I know of three logic programming languages: Prolog, Icon, and jq. jq is also a functional programming language, arguably, though jq is a bit of a toy (though a very useful toy!). To me Verse sounds like it shares a lot with Icon and jq: pervasive generators and backtracking, any values as truth / failure as falseness (in Icon in particular).
I am thinking of Alan Perlis' Quote "LIPS programmer know the value of everything and cost of nothing". If you abstract away execution details, you are making a tradeoff that makes the programmer's life easier when those details can be ignored, while making the programmer's life much harder when they can not be ignored.
I find this to be pretty prounouced in Prolog where the language encourages the programmer to only state what they want, when in practice, the programmer has to think about the process that will ensue from the request, and when there is a disonnace between the way the programmer think and what they write, things become messy. If you are going to abstract away something from me, you better be sure that you can deal with the details yourself.
50:34 Isn't what Simon is describing just a dependent type of sorts? You have properties/predicates that you want and can define a type that includes only objects that have this property. (Fortnite should probably use Agda instead /s)
Almost. Part of the inspiration is a system called "Ontic," which originated the "single semantic category for types and terms" in the sense Verse uses, and also Jason Hickey's work on "Very Dependent Types." One difference is that Verse's type system doesn't make the "closed world" assumption. That is, it can't make global consistency claims. It can only say something like "given all the code I have access to, at least IT is consistent."
@@paulsnively3377 I'm not sure I understand the distinction between global and local (?) constraints on types.
@@pooroldnostradamus Right. The most common (at least in type theory terms...) way to put it is there are two interpretations of "types," "Church types" and "Curry types." In the Church view, types define the semantics of the program: no types, no meaning. In the Curry view, an untyped program may very well have a meaning, and when you type that program, we hope and expect that the types reflect that meaning. When you stop and think about it, though, the Church view is unrealistic in a distributed setting: you can't know whether the "whole program" typechecks, because YOU don't have the "whole program," and in fact the "whole program" will change over time. So the Curry view it is! Now the wrinkle is that it's still the case that you don't have the "whole program." New bits will come and go; your own code will change in ways relevant to the types, etc. So all you can say in a distributed system from the Curry view is that, at any given moment in time, the (distributed) "program" you DO know about is consistent (in the logical sense implied by the Curry-Howard correspondence). The Verse verifier will provide "verification" in that sense.
amazing interview
If you have a line to Simon, I would be interested to know if there exists a version of CAS here in New Zealand. That part of the talk really resonated with me.
1:09:00 what a great talk on the perspective of how to better teach computer science and make it concrete. reminds of the white papers i've been reading play and education in general. you should get jonathan blow on to talk about jai and games for education.
I think they should have talked more about the differences between normal logic programming and functional logic programming.
I havent finished this video yet but im not sure i get the appeal/motivation for the functional logic programming. Isnt that what we already do, write functions with names that abstract the algorithm and return a result such that we dont have to understand the algorithm to use the function re. Example of x**2?
What are the fundamentals of computer science and should they be taught instead or in addition to the practical skills, like PowerPoint?
There was an interesting point about not being able to see the "what" immediately of an imperative program, i.e. to identify that a square root program is trying to compute the square root, whereas in a declarative program its the starting point, so you can just read it. But couldn't you equally say that in a declarative program, the "how" is not immediately obvious, and perhaps even hidden from you, whereas in an imperative program, its the starting point, so you can just read it...
In a just world Simon Peyton Jones would be the only person who is allowed to use comic sans.
I can't believe it! I feel honored to have been on the same podcast as SPJ!
You look just as excited as I would be introducing him
Ha, yeah, and that's me trying to keep it together. 😉
It's so funny that turing machines which depend so deeply om state and lambda calculus which doesn't know state can be proven to be equivalent
It's more that a turing machine is a description of state. If you look at it that way it's simply an alternate proof of the same things.
I've been wondering for a few years whether our Harvard/Vonn Neumann Machine architecture is a bottleneck for Lambda Calculus.
ruclips.net/video/UBgam9XUHs0/видео.html
Regarding "types" and verification: I wonder if SPT kept up with testing in Haskell, like quickCheck and property-based testing in general. And I wonder if SPT and Sweeney have thought about categories and homotopy. I'm sure he must have encountered "Computational Trinitarian" thought over the years...
Thanks again for the great interview.
Soo this whole buzz on verse is based on a feeling and "tim was always right" (he wasn't but whatever ) Yikes. It tries to solve no problem, just force a lot of people to deal with it because it's "cool"
verse sounds like lips a functional-logic complete lisp
Teach kids programming with small talk but modernize the environment first. It was great in the 80s but is dated now.
Purely functional programs are fundamentally slower than imperative programs by a factor of O(log(N))
Erm...do you have a reference for that? 🤔
Yes of course, if we expect that we are writing some kind of functional assembly language or some bs... Functional languages still have compilers, they can produce low-level instructions no better or worse than any high-level imperative language for similar algorithms.
FLiP. Is it
I have played with core.logic in Clojure which sounds quite similar to Verse?