An Existential Crisis Resolved: Type Inference for First-Class Existential Types

An Existential Crisis Resolved: Type Inference for First-Class Existential Types
Paper DOI: 10.1145/3473569
Presented at None, part of ICFP 2021
By Richard A. Eisenberg, Guillaume Duboc, Stephanie Weirich, Daniel Lee

[@officebatman9411]

Very nice video, thanks for uploading

[@tookerjerbs]

Thanks for the very clear explanations, I learned a lot. One question: It seems like existential types are just syntactic sugar for dependent pairs. Is there more to them than that?

[@thedeemon]

In a dependent pair the first element can be any term, so the pair looks like (x:A, y:B(x)). Here the first element is just a type, a bit simpler thing.

[@tookerjerbs]

@@thedeemon Thanks, that makes sense.