ICFP Video

Пікірлер

@mooncop 4 ай бұрын

first!1

@Aquaryus27 11 ай бұрын

You are the best! Nice speaking voice ❤

@cattime2044 11 ай бұрын

LOVE YOU ALWAYS SALAMAN ❤

@Aquaryus27 11 ай бұрын

You’re the best!❤

@asitisj Жыл бұрын

The sophomore part - does he mean ug or pg sophomore 😅

@okuno54 Жыл бұрын

If anyone else finds this by googling like I did... I also ported nanopass into Haskell and released it on hackage. Actually using it is a lot more readable, it does not generate partial functions (instead generating records that can hold bits where you need to provide code), you can define passes separately from languages (so that your passes can form a graph), and I even generate some documentation for the generated types and functions. I've just started using it in some larger examples, and ran into some slight issues, so I was just sitting down to make some breaking changes when I decided it was a good idea to check if anyone else somehow beat me to it. I guess technically yes, but actually no ;)

@capability-snob Жыл бұрын

I wonder if the "detailed tech report" is the paper by the same name as the video. It does have a lot of relations as described, but it's only 13 pages, including citations. Is there a deeper dive somewhere?

@vxanica Жыл бұрын

The repo is not accessbile

@alaindevos4027 Жыл бұрын

Shit recording & waste of time

@Max-se9fb Жыл бұрын

love the audio clipping for the first 30 seconds should have kept it going

@clarkkent1473 Жыл бұрын

Oof left panned audio ;-; *Turns on mono audio in accessibility settings*

@nick9323 Жыл бұрын

as @stevenspencer592 said "Expensive gibberish" (c)

@DrewLeSueur2 Жыл бұрын

cool video. Like the demo where you turned the line creation into a function very simply.

@densidad13 2 жыл бұрын

Last year I found about Paul's work and it has become an inspiration for my PhD research. A man sprouting so much love, its remarkable. Thank you for this tribute.

@alfonsobustamante6937 2 жыл бұрын

There is also, an alternative way to show that the identity is equal for both overlay and connection binary operations on graphs by using an identity discovered in the first decade of the 2000s.

@alfonsobustamante6937 2 жыл бұрын

There is actually another name for Descomposition in literature. There is an early Soviet Work on that subject.

@ainaaa1000 2 жыл бұрын

Can you give a reference?

@mooncop Жыл бұрын

we must know!

@BenHutchison 2 жыл бұрын

Such a typical Haskell talk.. the audio only works in the left channel, and it begins with "Let's say we have a type family defined like this..." . Lets say we wanted to learn about type families...?

@jonaskoelker 2 жыл бұрын

8:00 "with art students I've found that what most motivates them are questions of social justice" BWAHAHA. If the thing that most motivates them is not _art_ then what the fuck are they doing in art school? For the visual arts, surely the geometry of perspective drawing can inform artistic technique? In case of music, if you start at any key and go up or down by some fixed interval until you hit that key again, the only way to visit _all_ other keys is via a chromatic scale or the circle of fifths, because {1, 5, 7, 11} are the only numbers (mod 12) which are coprime with 12. Also I think music forms a semiring where addition is parallel performance of two voices (e.g. two instruments playing simultaneously) and product is sequential composition of two fragments (e.g. verse and then chorus). This is true because it's true of the underlying sound waves. (I don't know that there are many interesting equations you can derive from this, but at least it gives you more vocabulary and a new perspective for thinking about your art form.) Hey, when you double the frequency of a note the human ear and brain says "although they have some differences they're also equivalent in some ways" (see "octave equivalence"). When an instrument plays a tone with frequency f it typically also emits sounds at frequency 2f, 3f, ..., n*f at lower amplitudes. (The amplitude profile differentiates e.g. pianos from saxophones playing the same note.) It would be real nice, because music theory believes in this only-approximate truth, if repeated jumps from f to 3f could align with repeated jumps from f to 2f, i.e. if 2^n = 3^k for some natural numbers n and k. But that requires log_2(3) to be a rational number, which it isn't. But the continued fractions expansion of log_2(3) tells us how many notes to put into an octave to get a good approximation of this. For example, 12 is a good choice. We probably chose 12 before knowing about continued fractions. This means you want to go from f to 2f in 12 steps, each then being the 12th root of 2. You would love it if (2^(1/12))^7 = 1.5; in reality it's 1.49830707 which is pretty close. You could choose a set of non-uniform steps when you build your instrument, which makes a transposition from C major to D major sound more different than merely higher by two semitones. I could go on.

@wearysignal3957 Жыл бұрын

Please don't.

@valentinussofa4135 2 жыл бұрын

It is a great talk. Finally I understand what is homotopy type theory for Computer Programming.

@hanishsheoran8360 2 жыл бұрын

Whattt a genius ! Thanks for sharing

@chrisminnoy3637 2 жыл бұрын

Wondering what happened with the research...

@tejing2001 3 жыл бұрын

Nix's experimental ca-derivations feature actually moves it into that ideal spot. Cool 🙂

@takumicrary4396 3 жыл бұрын

Thanks

@takumicrary4396 3 жыл бұрын

Thank you

3 жыл бұрын

I'm very new to the field, what is a PL researcher? any bibliography to get started? thanks!

@shlomoweinstein2775 3 жыл бұрын

So, aaaahhhhh, ..., so, ahhhh, sniff, so....

@ytdlgandalf 3 жыл бұрын

So comprehensible. Nothing worldshattering yet nobody did it before, while almost all developers run into this stuff daily.

@insertoyouroemail 3 жыл бұрын

my left ear thanks you

@alisalehi7696 3 жыл бұрын

What is the best programming language for HoTT?

@amigalemming 3 жыл бұрын

Can we find the slides somewhere?

@heartofthunder1440 4 жыл бұрын

This is what’s happening here in the United States.

@codycharles7147 4 жыл бұрын

Play stupid games win stupid prizes

@JosiahWarren 4 жыл бұрын

Its now obvious that hott has very little practical programming value.

@epgui Жыл бұрын

I don't think that's totally true, or a very productive thought.

@isleofdeath 4 жыл бұрын

Absolutely cool if you can talk that freely and clear at the same time.

@andreyverbin 4 жыл бұрын

One important piece is missing - what is the structure of a space induced by a type? It is not immediately clear that such a space could have reasonable topology and paths at all. Maybe all we can do is pointwise topology? Or we can imagine infinite number of topologies - thus a path in one might not be a path in another. The there is a jump from “type is a space, points are elements of a type” to “paths between types”. For such a path between types we need a space where points are types themselves which was never introduced. With these basic things lacking content of the whole lecture seems opaque to me.

@homology 3 жыл бұрын

You never really descend on the "topology" level. Note the contrast between "topology" and "homotopy": the latter does not deal with points and topological structures (sets of opens). Now, if one wants to go to homotopy theory from HoTT and interpret types as [homotopy classes of] spaces, then there are different models, such as Kan simplicial sets, which the Univalence Exion owes its existence to. A path between types takes place in the "universe type" U.

@andreyverbin 3 жыл бұрын

@@homology I don't think I fully understood your comment, too mathy for my :) I guess if you have a path then you must have a structure on a set that would allow it. The simplest structure of this sort I can think of is topology. In other words how do you move along the path?

@homology 3 жыл бұрын

@@andreyverbin Homotopy in HoTT is synthetic, meaning that it is not constructed inside some ambient theory (e.g. via sets with structures), but rather is "already there". Compare with synthetic geometry (working in a thing with Euclidean axioms) vs analytic geometry (working in a set of tuples of numbers which one thinks of as coordinates). In particular, paths in HoTT are a primitive, built-in notion. By definition they are just elements of identity types (so one writes p: a = b). Then "transport along a path" is a function whose existence follows formally from the definition of an identity type (which in turn is defined by its induction principle, much in the way the natural numbers are defined as the type enabling induction).

@silent9027 4 жыл бұрын

It is I THE STEPPERS! also i have not got a superb on lockstep yet

@johannesberger8641 4 жыл бұрын

You are secretly assuming C to be concrete (which is probably ok, since you are a programmer), right? It just was not mentioned explicitly, and so the statement at 11:25 was confusing at first, i.e. the identity is not a functor from C to Set. But it is of course if C is concrete.

@strangeWaters 3 жыл бұрын

Doesn't it only need to be locally small?

@rudyhoffman1683 4 жыл бұрын

What is this psychotic satanic crap? And who is this soy boy?

@mgetommy 4 жыл бұрын

helped my understanding of rust mightily

4 жыл бұрын

Fun fact: from 0:00 to 20:00 there are 176 "eerm"s in the talk

@CyberneticOrganism01 4 жыл бұрын

This is pretty deep stuff, it took me a long time to understand the background ideas, such as the Curry-Howard isomorphism and homotopy theory. From the Curry-Howard correspondence, type theory corresponds to propositional logic. But we also need predicate logic to describe more complex stuff. So, to handle predicates we need types to have subtypes, similar to sets having subsets. Such structures (ie, the predicates) are "fibrations" over the base set, borrow the idea from algebraic topology. Now, it has long been known that propositional logic is more or less "isomorphic" to topology (ie, the structure of open sets). So the fibration of predicate logic above is over the base topology of propositional logic. Thus the idea of homotopy theory enters because it characterizes some properties about the predicates and the underlying propositions.

@ZekeFast 4 жыл бұрын

I felt like I'm back to university and hate math again. Does it mean I have to fast forward 3 years and I will fall in love with those ideas because I find a reasonable explanation to them written by original authors and not this in a world nonsense rubbish. I don't know ... yet!