System FC

[FrankBro]

I've recently been looking around at System FC, which is what is used in haskell. I don't know if you've heard of it but it's interesting.

https://www.youtube.com/watch?v=2IZQx7WNOMs
https://www.cs.uoregon.edu/research/summerschool/summer13/lectures/FC_in_GHC_July13.pdf

[tomprimozic]

Hi FrankBro!

Thanks for pointing this out! I was vaguely aware that GHC used some form of evidence of type equality, but I didn't know any specifics. However, skimming through the presentation you linked, it seems that System FC is used mainly during compilation, by the GHC intermediate language. In my experiments, however, I focused on type systems with a form of type inference, which System F (and its extensions) lacks. There are ways of type inference for GADTs, but none of them is complete.