A Type System From Scratch - Robert Widmann

[@RobertWidmann]

Hi, Robert here. Just wanted to correct a couple of my own mistakes here - I was way too generous putting Swift up there with System F (λ2) considering we don't really have kinds. But you can do some terrifying things to try and encode them nonetheless. - The notation for subtyping is not usually a "carat and a colon", it's usually a less-than and a colon (

[@RobertWidmann]

Chris Eidhof also saved a question off-screen about the section where I mentioned that you can sort of read the stacked typing judgements (@13:47) from bottom-to-top. The answer is really, like everything here, you can read it multiple ways. If you read top-to-bottom you get to follow a deductive series of arguments that lead you from small premises to bigger conclusions. If you read bottom-to-top you can break a large problem down into its sub-parts and work your way backwards towards what led you there. I'm personally a fan of reading them in a spiral where you start at the left side of the conclusion then read the premises, then read the right hand side. All will lead you to a different viewpoint. All are equally valid.

[@emanueltesar2388]

@@RobertWidmann Hi :) I really enjoyed your talk and really liked the type cube. I would be interested in learning more about type systems in general. Can you share some resources to learn from? Books, talks etc...? I am also up for the proofs of the the complexity (as you just mentioned what is NP, undecidable...). Thank you :)

[@I_lovefood831]

hello cousin

This went over my head. I'll come back in a year or two and see if I understand anything.

[@yixe2253]

reminder, its been over a year

[@kevkev6798]

Reminder, it’s been two years

[@louisthibault555]

Where did you get stuck? Can I help?

[@jpratt8676]

It's been four years. How'd you go?

It's too dense and long to keep my attention. Good thing is that 4 years later I now know that I have ADHD, so it makes sense.

[@pibob7880]

It's always mind blowing that arranging/abstracting data into different forms can save much computation.

[@blacklistnr1]

Funny that swift assumes that the human knows the types (=> easy enough for sleepy programmer to deduce), but then runs into exptime while solving 60 rules. Mayybe, just maybe.. there is another simpler ruleset which runs in like O(N), because if I have to read an expression and its types more than 3 times to figure out the type I'll just *table flip* and switch language.

[@bibliusz777]

surprisingly good talk

[@sunofabeach9424]

god bless english, the best type system ever invented. can't say the same about Swift

[@mrmaniac9905]

In what world does calling expressions "applications" make sense...?

[@valshaped]

It's function application: applying f to x is literally f(x)