Impredicative Types - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

James King

I just watched SPJ's updated on Impredicative Types thanks to Chalmers: http://chalmersfp.org/

The examples were small for good reasons. I'm curious where else this extension could be used -- is being able to type apply a quantified variable some thing that Haskell programmers frequently desire?

It was amazing be able to watch an SPJ talk live! While I enjoy conferences I can't always travel to where they take place. I hope SPJ may consider doing more talks in this manner if it wasn't too painful or weird for him.

Peter Kjeld Andersen

I hope the recording turns out okay. I couldn't get audio :(

Alex Chapman

I have come up against GHC telling me that it doesn't support impredicative polymorphism on several occasions, mostly in trying to use the machines library. I think I had to use newtype wrappers around things to make it work. So to not have to do this would be nice.

Chris Wendt

Another example: I needed impredicativity last week when I was attempting to write a control function that took a list of callbacks as an argument. I deleted the broken implementation and wrote it some other way.

Alex Chapman

I think it's something that if we didn't have to work around, we would use all the time.

TheMatten

Guess guys what got merged :tada: : https://gitlab.haskell.org/ghc/ghc/-/commit/97cff9190d346c3b51c32c88fd145fcf1e6678f1

This patch implements Quick Look impredicativity (#18126), sticking very closely to the design in A quick look at impredicativity, Serrano et al, ICFP 2020 The main change is that a...
TheMatten

(Coming to your GHC in 9.2 :big_smile: )

Torsten Schmits

then we can use it in production in 10 years!