Don Syme is a pretty cool guy from what I’ve seen online too. He enjoyed supporting and attending Migrateful (UK charity where refugees/asylum seekers teach cooking classes) which I’m appreciative of in particular.
System F is a polymorphic lambda calculus, it's more theoretical than practical (typing must be explicit or type inference may be impossible) but a restriction of its typing scheme is one you may have heard of, and the Hindley-Milner type inference algorithm works for it.