1.1 KiB
https://gist.github.com/CMCDragonkai/b203769c588caddf8cb051529339635c
http://iveselov.info/posts/2012-08-30-existential-types.html
https://markkarpov.com/post/existential-quantification.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.