Adventure with Types in Haskell - Simon Peyton Jones (Lecture 2)

Recorded at Oregon Programming Languages Summer School 2013. www.cs.uoregon.edu/research/s...
Lecture 1 Slides: www.cs.uoregon.edu/research/s...
System F in GHC: www.cs.uoregon.edu/research/s...
Kinds and GADTs: www.cs.uoregon.edu/research/s...
Type Inference: www.cs.uoregon.edu/research/s...
Fun with Type Functions: www.cs.uoregon.edu/research/s...

[@jasonfeingold2314]

He consciously has one foot in the classroom and one foot on the shop floor and this makes me happy.

[@collinrea6183]

38:19 is when Higher Kinded types really clicked for me. So powerful.

[@okuno54]

1:01:18 I try to treasure my uneasy feelings, and just wait until it seems so simple and beautiful that it's impossible not to love it. This is a great stance for PhDs to take!

[@adamyin2537]

38:16 I've spotted the free monad!

[@okuno54]

1:04:33 Ooooh, much better than the blub argument

[@yankumar5280]

thanks for sharing jasonofthel33t

[@Kram1032]

All this discussion about Types, Kinds and Sorts makes me curious how, if at all, the recent HoTT will change things. If I'm not mistaken, that would be a (the?) way to unify all of this in a comparatively straight forward way. Though of course it's way too new to really know these things yet. But Homotopic Haskell or how ever it would be called could be rather interesting.

[@Kram1032]

***** I know that they do. However, those are, as by this very lecture, languages that "require a PHD" and it would be cool to have in a "practical language". My understanding of what the univalence axiom will do, thus far, was that it would do a whole lot, simplifying a ton of things that have to do with "higher order" types. The problem, however, is that nobody quite knows how to express the univalence axiom in a computational manner, so it's not yet known if it'd even work for this. Though my understanding is very limited so I might be completely wrong. The other thing with at least Agda and Coq (I don't know whether this is the case with Idris), to my knowledge, is that they are not Turing complete in that they don't allow programs that are not sure to terminate. They are great for proofs, which they also are designed for, but writing programs that involve potentially infinite loops, like you might want to have in the case of an OS that shouldn't just randomly terminate and shut down your computer, wouldn't be possible with them. - Once again, though, my understanding is limited...

[@Kram1032]

Heh, I suppose in the end it's just what you're used to :D I suppose, first and foremost, HoTT will be interesting for mathematics, to potentially significantly improve prove-checkers. Afaik some of the features that were added to Coq and Agda to begin to support HoTT already significantly made certain constructions much more efficient, which quickly becomes important. But I'd be surprised if there was no interesting lesson to be learned for other programming languages of which proof checking isn't the primary concern. Anyway, it's way too early to know this already. We'll see about that in, say, the coming decade or so.

[@jethrolarson]

TIL even Haskell people think they're moderate

[@wliaputs]

what do you mean lol

[@noninvasive_rectal_probe8990]

Oh my crap!!! He's wearing shorts 🤢