Without types, yes the let binding is effectively syntactic sugar over an abstraction and application. However, in the simply typed lambda calculus which this series gets to later, there are slightly different typing rules to do with polymorphism that let bindings have (which can't be applied to abstraction as easily - there are some complexity proofs but I don't get into them in this series).

Glad you enjoyed it! And thank you for taking the time to leave such a kind comment :)

The expression is: (\x -> (y -> x)) 1 2 We apply things left to right. If I make the brackets explicit: ((\x -> (y -> x)) 1) 2 This means the x takes the value 1, so the bit inside the outer bracket above becomes (y -> 1), leaving the expression as: (\y -> 1) 2

Thanks! Hopefully you enjoy the rest of the series too :)

@@adam-jones Yes, indeed, watched the whole lot!

Close, but not quite. It's actually that the type variable _is_ bounded everywhere else it is used. That's because where it is not bounded the type constraints should remain attached. Maybe this JavaScript code helps as an analogy: ``` // pretend this JS represents the context... let x, y; // ...and functions represent assignments in the context const t1 = () => x; const t2 = () => x; const t3 = () => y; const t4 = (y) => y; ``` Generalisation in this analogy would be like moving down the let declaration into the function. We could not generalise the x in t1 because it shares a reference with t2. i.e. if we moved the declaration then t2's x would be undefined. We could generailse the y in t3 because it is bound everywhere else it appears in the context (t4). i.e. if we moved the declaration all other definitions would be fine.

Thanks so much for taking the time to provide detailed feedback and tips! Agree, on reflection the audio especially in the earlier videos is quite poor. I think I got a bit better towards the end of the series at all of speaking + recording + postprocessing, although still far from perfect. The tip about speaking further from mic and projecting more makes a lot of sense and I hadn't heard of that before. Will take that and all the other stuff on board when making any future recordings.

I REALLY appreciate you going to the effort to make those "stack" diagrams that clearly delineate each sub-expression, like at 7:45

@@gloverelaxis Thanks for the kind feedback, glad these were helpful :)

Yep, I think your proposed approach sounds good. To implement this in practice based on the code in the video, you could use the W algorithm to get a monotype and then call generalise with an empty context to get the function's generic type (this might not work - just off the top of my head). I'm a software engineer (although right now doing some other stuff short term that is closer to technical advising). This series was just an interest on the side, as I'd learnt it and figured some of the other resources weren't quite as comprehensive and practical as this. :)

Yup, I agree it's a bit of a weird one and doesn't line up with set logic in my head. It seems to be convention, even if a little confusing. If someone does know why it's that way round would be keen to learn :)

I don't know why it is that way, but I like to remember it by thinking that in the context of type inference the more desirable type is the least general type. So it is the best/greatest of the two and that is why ⊑ points towards it. But I have to recall that rule every time I see ⊑, so to me it is the wrong way around too!

Good spot! Thanks for the correction. And glad you're finding the playlist helpful.

So in this system `List` is a type function, which can be applied to a monotype to form a monotype. `List Bool` is a monotype: it's the type function `List` applied to the type function (that accepts no arguments) of `Bool` `∀T . List T` is a polytype: but it's not that it uses a List that makes it such. It's that it has a for-all quantifier. Technically something like `∀T . Bool` is a polytype (even if the for-all quantified variable isn't actually used - although it's a bit pointless and could then be reduced to just `Bool`). --- Maybe another way of looking at this is that `List ≈ Array`, and `∀T . List T ≈ Array<T>`? But these concepts don't always map quite right between languages.

Thanks for the kind comment! The full playlist is here: kzbin.info/aero/PLoyEIY-nZq_uipRkxG79uzAgfqDuHzot-

Thank you for the kind comment! Glad they are helpful.

Thanks for the question! I assume you mean at 1:18? Here I was using union in the sense that if you view it as a set of mappings, S3 is effectively all the mappings in S1 and all the mappings in S2. I didn't mean it in any very technical specific sense here - sorry for any confusion caused. In TypeScript I guess this would be similar to spreading all the substitutions in (although in general this pattern doesn't work - as explored later in the video).

@@adam-jones Thanks for the clarification! :-)

Thanks for the kind comment! Glad the videos have been helpful :)

Glad you're happy with the series, and thanks for taking the time to leave a comment :) Does it look like the direction it builds up to is what does interest you? Or would you like to learn other things that the series doesn't cover?

Thanks for the kind words Marc, I appreciate the time you've taken to leave a comment! Am glad you found the series easy to follow and are finding the topic interesting. I don't have much more similar teaching content on other social media at the moment unfortunately, but I guess maybe will add more over time :)

I guess it's maybe like in algebra where you might be given some simultaneous equations like: 2x + 3y = 19 x + 2y = 23 And here, because it's not quantified (i.e. x and y are free variables) they are actually less general: they're fixed by other constraints. Whereas in something like: ∀x. ∀y. x^2 - y^2 = (x - y)^2 this ends up being more general, in that x and y could be many more different things and this expression still holds. Does this help at all?

Glad it helped, and thanks for the kind comment :)

Glad you enjoyed the series, and thanks for taking the time to comment :)

Thanks for the kind feedback, I appreciate it!

Thanks! 🙌

Thanks for the feedback! Agreed my psuedo-Python at 1:54 is a little inconsistent as to whether the context is a list or set. I think I used a list here as in previous videos I described the context via its BNF grammar that builds it up as a list, but agreed a set or map would probably be the more sensisble data structure - and in fact in later videos where I impement Hindley-Milner in TypeScript I use a map for the context.

@@adam-jones Cool I haven't watched that far yet. I just felt this content deserved some tickling of the KZbin algorithm with some like and comment interaction. Why Typescript and not ReScript (or Elm or Purescript)?

@@charstringetje Haha thanks for playing the algorithm :) Regarding language choice, I was very tempted to do it in rescript or Purescript. However, I chose TypeScript for two main reasons: 1. I thought it would be a language that more people would know, especially as I wanted this series to be accessible to people without a significant functional programming background. 2. I'm more familiar with TypeScript (and implemented HM in TypeScript once before), and given that I already am dealing with a tricky concept didn't want to make it harder on myself by using a language I was less familiar with! (although I appreciate mapping the HM algorithms into a more functional language might be nicer with better pattern matching features).

Glad the implementation videos are helpful! And thank you for your feedback and kind words - the videos can take quite a while to plan, record and edit so your comment means a lot.

I think you're correct here! To maybe help clarify a bit: 1. Our context Γ, is a list of assignments. And assignments are mappings from expressions to types, including polytypes (see kzbin.info/www/bejne/npLZl6aAgLKYkKs for a recap). So Γ(x) could be a polytype. You're right that they can only be created by let bindings (and we could imagine somehow our program is surrounded by let-in bindings defining our global helper functions, like Haskell's prelude). 2. However, algorithm W returns a tuple [Substitution, Monotype]. So to convert Γ(x) from a polytype to a monotype we need to instantiate it. We do this by replacing all the for-all quantified variables in the polytype with fresh variables. Exactly like your example in your edit, provided t0 and t1 were type variables not free anywhere else in our existing types (so they don't have any other constraints beyond how they're used in this type). 3. You're right at this point we don't know t0 and t1. However, it will be refined later by combining other constraints when we continue with the algorithm. --- For example, lets say we have `id true` (where id is the identity function). When we look at the id type from the context, we might get a type `forall a. a -> a`. We first instantiate and get something like `t0 -> t0`. At this point, we don't know what t0 is, but that's okay. So the next step is to look at the argument to id, which is 'true'. Let's say we look this up in the context, and find it has type `Bool`. Then we take a step back and look at the two with the function application rule. At some point we create a new type variable beta we'll call t1, and unify our argument to beta against the function type: unify(t0 -> t0, Bool -> t1) If we look at what has to match, we see t0 ~ Bool (because they're both on the left of the arrow) and t0 ~ t1 (because they're both on the right of the arrow). And by transitivity, Bool ~ t1. So we could get the unifying substitution { t0 |-> Bool, t1 |-> Bool }. This then gives us the overall type of `Bool -> Bool` for the function. Then we can just take the return type beta which is `Bool`. Hopefully this example helps show how that inst rule plays in to everything else, and how the constraints introduced by our fresh type variables get combined elsewhere.

Glad it helped! And congrats on passing :)

Thanks for your feedback! Happy you have been enjoying the series. More videos are being released now and over the next few weeks.

Thanks for your comment! Agreed that I think there are proabably more people who could do with finding out about these videos. I'm hoping long-term this series is a useful resource for people coming to this topic, and that people share it with others/list it as useful watching etc., so expect the views to (slowly) grow over time.

Glad you've found the series helpful! Algorithms videos are coming out now and over the next few weeks :)

Glad it was useful Samy!

Thanks for the feedback Affandy, glad it was useful 🙌

I agree, the lambda calculus statement doesn't read perhaps as clearly on first viewing than the imperative alternative which might look like: ``` def odd: return mod(x, 2) == 1 return odd(3) ``` However, in this series the purpose of using Lambda calculus is that it's a relatively simple syntax that can be analysed (relatively) easily in terms of typing rules. By simple here, I mean in the number of building blocks you have to construct expressions - we've just got variables, application, abstraction and let-in bindings (as opposed to an imperative language, for example where you have variables, application, abstraction, assignments, return statements, if statements, for loops, while loops, switch statements etc.). This simpler set of building blocks makes it easier to analyse in terms of formal proofs, definitions and algorithms on the language itself (e.g. typing proofs, the defintion of a free variable, type inference algorithm W)

@@adam-jones Yes ... in other words it's for nerd credentials.

@@velcomat9935 did you miss the part where it's easier to analyse? That also includes "easier to analyse *for computers*". That's very useful for language implementers.

​@@velcomat9935 He even gave you a perfectly well-explained reason for why lambda calculua is good and you just ignored it

@@TheRiseLP ... and those reasons concern only those who live in that far off distant land called "Academia", or is it called "Utopia", or maybe it's called "Atlantis", or some such name anyway. PS: You're not from -there-, are you?

Thank you for the kind feedback Jawad! I initially planned out a series all the way to algorithm W, but recently haven't had much spare time to make these videos so I've fallen behind a bit. I'll try to continue the series and post some videos within the next couple of weeks - that probably wouldn't have happened if not for your comment, so thank you.

@@adam-jones That would be awesome, glad I could help

It should be io, but my best guess is that b should actually have been "ho" and then applying the substitution would result in "oi", but that's just my best guess what @Adam Jones actually intended to do

Good spot! There is an error at 1:10, you are correct S(b) = io. @Gustav is right in that I meant to write b = ho here, as case S("ho") = hi. I will try to edit or reupload the video soon to correct this mistake.

I've edited the video to remove this section with the error now. Thanks again Emi and Gustav!