diff --git a/existential-types.md b/existential-types.md index b937ddd..b8a4048 100644 --- a/existential-types.md +++ b/existential-types.md @@ -1,3 +1,22 @@ https://gist.github.com/CMCDragonkai/b203769c588caddf8cb051529339635c http://iveselov.info/posts/2012-08-30-existential-types.html + +Great explanation by Anupam Jain in FPNCR Telegram channel :) + +Everything gets a forall. + +Basically if you see a free variable x in a type signature, assume there’s a +*forall x* in front of the signature. + +Free variable is just a fancy way to say an undeclared variable. Where *forall* +is the way we declare variables. So if the signature is *foo :: a -> Int*, +the *a* is free because it was not introduced first with a *forall*. + +*forall* at type level is like a lambda (\) at the value level. It basically +says somehow I will be given a type and then rest of the implementation can +depend on that type. And in fact some languages like Dhall make it explicit +where they accept an actual type parameter instead of making it implicit + +In Dhall it would be something like ‘foo : a:Type -> val:a -> Int’ +It says foo takes a type, a value of that type, and gives you an Int back.