Add a nice explanation on existential-types

Signed-off-by: Sanchayan Maity <maitysanchayan@gmail.com>
This commit is contained in:
Sanchayan Maity 2020-06-06 18:31:17 +05:30
parent b1ef1705d3
commit ce6e56a49e
1 changed files with 19 additions and 0 deletions

View File

@ -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 theres 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.