2020-04-20 16:42:08 +02:00
|
|
|
|
https://gist.github.com/CMCDragonkai/b203769c588caddf8cb051529339635c
|
|
|
|
|
|
|
|
|
|
|
|
http://iveselov.info/posts/2012-08-30-existential-types.html
|
2020-06-06 15:01:17 +02:00
|
|
|
|
|
2023-03-20 16:33:04 +01:00
|
|
|
|
https://markkarpov.com/post/existential-quantification.html
|
|
|
|
|
|
|
2020-06-06 15:01:17 +02:00
|
|
|
|
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.
|
