From ce6e56a49e9baecdf49ca46698534b3396928930 Mon Sep 17 00:00:00 2001 From: Sanchayan Maity Date: Sat, 6 Jun 2020 18:31:17 +0530 Subject: [PATCH] Add a nice explanation on existential-types Signed-off-by: Sanchayan Maity --- existential-types.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) 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.