So thankful that LambdaConf organizers decided to get confreaks to come to record the sessions. This talk was only helpful to me years after I attended this talk. Also thankful to this speaker for coming to share his knowledge. So nice.
It's always frustrating that the questions from the audience are (almost) not audible. Please provide them as subtitles (embedded in the video itself, not (only) in the cc) or as voice-over. Thanks
I absolutely did not understood the second task and this Elem type. I spend couple of hours to understand this type and how it correlates with function get and I failed. But nevertheless, when I opened editor and started writing code I somehow implemented working function get. Indeed, there is only one way to do this, but even having written a function, I do not fully understand how it works and how in general it was possible to come up with such a thing. To be honest, when I finished this function, I didn't even immediately understand how to use it. That feeling when you managed to do something, but you don't feel any satisfaction from it.
It's an idea that's natural to people who are used to theorem proving, but not obvious to most programmers. The idea is that here you can't just pass in an arbitrary number, because you don't know what type the element at that index is, or if it even exists. So here you pass a "witness" (of type Elem ts t) that you know there's an element of type (t) in the list of type (HList ts). The structure of the type (Elem ts t) is similar to unary Natural number (e.g. N ::= Z | S N), but richer, encoding the inductive definition of what it means to know that an element is in the list.
So thankful that LambdaConf organizers decided to get confreaks to come to record the sessions. This talk was only helpful to me years after I attended this talk.
Also thankful to this speaker for coming to share his knowledge. So nice.
Eisenberg is such an amazing Haskell teacher. Really enjoyed his series in @Tweag, hope I could get more of these
can confirm that in 2024, GHC handles things nicely without complaining about bogus incomplete patterns :)
Superb tutor!
Very nice tutorial, Thank you!
It's always frustrating that the questions from the audience are (almost) not audible. Please provide them as subtitles (embedded in the video itself, not (only) in the cc) or as voice-over. Thanks
I absolutely did not understood the second task and this Elem type. I spend couple of hours to understand this type and how it correlates with function get and I failed. But nevertheless, when I opened editor and started writing code I somehow implemented working function get.
Indeed, there is only one way to do this, but even having written a function, I do not fully understand how it works and how in general it was possible to come up with such a thing. To be honest, when I finished this function, I didn't even immediately understand how to use it.
That feeling when you managed to do something, but you don't feel any satisfaction from it.
It's an idea that's natural to people who are used to theorem proving, but not obvious to most programmers.
The idea is that here you can't just pass in an arbitrary number, because you don't know what type the element at that index is, or if it even exists. So here you pass a "witness" (of type Elem ts t) that you know there's an element of type (t) in the list of type (HList ts). The structure of the type (Elem ts t) is similar to unary Natural number (e.g. N ::= Z | S N), but richer, encoding the inductive definition of what it means to know that an element is in the list.
Please mic the audience next time :)
+Echo Nolan with headphones they are audible, just
the repo github.com/goldfirere/glambda