Great talk! On a side note, this is probably the most advanced work on General Artificial Intelligence so far."Type-Driven Program Synthesis" is obviously the right path. Let the people from machine learning do they deep neural network stuff, their will never get it :)
I'm not so sure the "let there be instagram" future is as inconceivable as she thinks. Sure there's the essential complexity of describing what "instagram" is (and is not), but scaling is just an optimization problem. For example, the (quite impressive) negation normal form function was a specific case of a structure-preserving transformation between two related Initial Algebras (the recursive types and the measure). Functional programs are an initial algebra, C++ programs are an initial algebra, and machine executable programs are an initial algebra. Statically and dynamically linked libraries are a collection of members of an initial algebra. Compilation and optimization is thus a structure-preserving map between initial algrbras that minimizes resource utilization. Even scarier for the mathematicians in the room, these algebraic refinement types are an initial algebra. Synthesis itself is something of a structure preserving map between initial algebras. This is good stuff.
Geez. Just watched this twice, and I'm gonna be recommending the living frick out of this. Even if it's not directly and broadly applicable, it's still a fantastic pattern.
13:07 I don’t understand this. Looks to me like you’re comparing a single element of a list (the head) with an entire list. How is that operation defined? I mean, “v” covers several elements in “t”, so how can we compare “v” to “h”? I guess it would make sense to just compare “h” with the head element of “v”, but I’m not sure if that’s how it’s done.
![[ICFP'23] Explicit Refinement Types](/img/1.gif)
Great talk! On a side note, this is probably the most advanced work on General Artificial Intelligence so far."Type-Driven Program Synthesis" is obviously the right path. Let the people from machine learning do they deep neural network stuff, their will never get it :)
Yeh I am looking at merging this with Optimal Ordered Problem Solver so you could exploit old solutions and do meta-searches. Looks promising
Agree. DNA and RNA work with refinement types. Methylation is a „epigenetic“ refinement.
I'm not so sure the "let there be instagram" future is as inconceivable as she thinks. Sure there's the essential complexity of describing what "instagram" is (and is not), but scaling is just an optimization problem.
For example, the (quite impressive) negation normal form function was a specific case of a structure-preserving transformation between two related Initial Algebras (the recursive types and the measure). Functional programs are an initial algebra, C++ programs are an initial algebra, and machine executable programs are an initial algebra. Statically and dynamically linked libraries are a collection of members of an initial algebra. Compilation and optimization is thus a structure-preserving map between initial algrbras that minimizes resource utilization.
Even scarier for the mathematicians in the room, these algebraic refinement types are an initial algebra. Synthesis itself is something of a structure preserving map between initial algebras.
This is good stuff.
Great talk, cheers
Great talk!
Awesome talk!
generation is very similar to idris 2
Geez. Just watched this twice, and I'm gonna be recommending the living frick out of this. Even if it's not directly and broadly applicable, it's still a fantastic pattern.
Is Haskell the pinnacle of creation? 😁😁😁
13:07 I don’t understand this. Looks to me like you’re comparing a single element of a list (the head) with an entire list. How is that operation defined? I mean, “v” covers several elements in “t”, so how can we compare “v” to “h”? I guess it would make sense to just compare “h” with the head element of “v”, but I’m not sure if that’s how it’s done.
Ignore `t` here, it is irrelevant in thinking about what `v` is.
The refinement `{ v:a | h
Oh. It's a logic programming language that saves the proof.