Encoding universal types in terms of existential types?
In System F, the type exists a. P can be encoded as forall b. (forall a. P -> b) -> b in the sense that any System F term using an existential can be expressed in terms of this encoding respecting the typing and reduction rules.
In "Types and Programming Languages", the following exercise appears:
Can we encode universal types in terms of existential types?
My intuition says that this isn't possible because in some way the "existential packaging" mechanism simply isn't as powerful as the "type abstraction" mechanism. How do I formally show this?
I am not even sure what I need to prove to formally show this result.
lambda-calculus existential-type type-theory system-f
asked Nov 19 '18 at 13:33
Agnishom ChattopadhyayAgnishom Chattopadhyay
8611020
add a comment |
In System F, the type exists a. P can be encoded as forall b. (forall a. P -> b) -> b in the sense that any System F term using an existential can be expressed in terms of this encoding respecting the typing and reduction rules.
In "Types and Programming Languages", the following exercise appears:
Can we encode universal types in terms of existential types?
My intuition says that this isn't possible because in some way the "existential packaging" mechanism simply isn't as powerful as the "type abstraction" mechanism. How do I formally show this?
I am not even sure what I need to prove to formally show this result.
lambda-calculus existential-type type-theory system-f
asked Nov 19 '18 at 13:33
Agnishom ChattopadhyayAgnishom Chattopadhyay
8611020
You might want to look into skolemization: en.wikipedia.org/wiki/Skolem_normal_form
– Juan Pablo Santos
Nov 19 '18 at 16:34
1
@JuanPabloSantos I fail to see the connection
– Agnishom Chattopadhyay
Nov 19 '18 at 16:41
I can't prove that either. At best, I can check that the analogous strategy fails. That encoding for "exists" is a consequence of YonedaT ~ (forall a. (T->a)->a)where we can takeT = exists b. f band exploit the type isomorphism(T->a) ~ (forall b. f b -> a), leading to the encoding above. The analogous strategy would be using co-YonedaT ~ (exists a. a * (a -> T)), but hereTis in positive (covariant) position, so choosingT ~ (forall b. f b)does not allow to turnforallinto someexists.
– chi
Jan 11 at 14:05
add a comment |
In System F, the type exists a. P can be encoded as forall b. (forall a. P -> b) -> b in the sense that any System F term using an existential can be expressed in terms of this encoding respecting the typing and reduction rules.
In "Types and Programming Languages", the following exercise appears:
Can we encode universal types in terms of existential types?
My intuition says that this isn't possible because in some way the "existential packaging" mechanism simply isn't as powerful as the "type abstraction" mechanism. How do I formally show this?
I am not even sure what I need to prove to formally show this result.
lambda-calculus existential-type type-theory system-f
asked Nov 19 '18 at 13:33
Agnishom ChattopadhyayAgnishom Chattopadhyay
8611020
In System F, the type exists a. P can be encoded as forall b. (forall a. P -> b) -> b in the sense that any System F term using an existential can be expressed in terms of this encoding respecting the typing and reduction rules.
In "Types and Programming Languages", the following exercise appears:
Can we encode universal types in terms of existential types?
My intuition says that this isn't possible because in some way the "existential packaging" mechanism simply isn't as powerful as the "type abstraction" mechanism. How do I formally show this?
I am not even sure what I need to prove to formally show this result.
lambda-calculus existential-type type-theory system-f
lambda-calculus existential-type type-theory system-f
asked Nov 19 '18 at 13:33
Agnishom ChattopadhyayAgnishom Chattopadhyay
8611020
asked Nov 19 '18 at 13:33
Agnishom ChattopadhyayAgnishom Chattopadhyay
8611020
edited Nov 19 '18 at 16:40
Agnishom Chattopadhyay
asked Nov 19 '18 at 13:33
Agnishom ChattopadhyayAgnishom Chattopadhyay
8611020
asked Nov 19 '18 at 13:33
Agnishom ChattopadhyayAgnishom Chattopadhyay
8611020
asked Nov 19 '18 at 13:33
Agnishom ChattopadhyayAgnishom Chattopadhyay
8611020
8611020
You might want to look into skolemization: en.wikipedia.org/wiki/Skolem_normal_form
– Juan Pablo Santos
Nov 19 '18 at 16:34
1
@JuanPabloSantos I fail to see the connection
– Agnishom Chattopadhyay
Nov 19 '18 at 16:41
I can't prove that either. At best, I can check that the analogous strategy fails. That encoding for "exists" is a consequence of YonedaT ~ (forall a. (T->a)->a)where we can takeT = exists b. f band exploit the type isomorphism(T->a) ~ (forall b. f b -> a), leading to the encoding above. The analogous strategy would be using co-YonedaT ~ (exists a. a * (a -> T)), but hereTis in positive (covariant) position, so choosingT ~ (forall b. f b)does not allow to turnforallinto someexists.
– chi
Jan 11 at 14:05
add a comment |
You might want to look into skolemization: en.wikipedia.org/wiki/Skolem_normal_form
– Juan Pablo Santos
Nov 19 '18 at 16:34
1
@JuanPabloSantos I fail to see the connection
– Agnishom Chattopadhyay
Nov 19 '18 at 16:41
I can't prove that either. At best, I can check that the analogous strategy fails. That encoding for "exists" is a consequence of YonedaT ~ (forall a. (T->a)->a)where we can takeT = exists b. f band exploit the type isomorphism(T->a) ~ (forall b. f b -> a), leading to the encoding above. The analogous strategy would be using co-YonedaT ~ (exists a. a * (a -> T)), but hereTis in positive (covariant) position, so choosingT ~ (forall b. f b)does not allow to turnforallinto someexists.
– chi
Jan 11 at 14:05
You might want to look into skolemization: en.wikipedia.org/wiki/Skolem_normal_form
– Juan Pablo Santos
Nov 19 '18 at 16:34
You might want to look into skolemization: en.wikipedia.org/wiki/Skolem_normal_form
– Juan Pablo Santos
Nov 19 '18 at 16:34
1
1
@JuanPabloSantos I fail to see the connection
– Agnishom Chattopadhyay
Nov 19 '18 at 16:41
@JuanPabloSantos I fail to see the connection
– Agnishom Chattopadhyay
Nov 19 '18 at 16:41
I can't prove that either. At best, I can check that the analogous strategy fails. That encoding for "exists" is a consequence of Yoneda
T ~ (forall a. (T->a)->a) where we can take T = exists b. f b and exploit the type isomorphism (T->a) ~ (forall b. f b -> a), leading to the encoding above. The analogous strategy would be using co-Yoneda T ~ (exists a. a * (a -> T)), but here T is in positive (covariant) position, so choosing T ~ (forall b. f b) does not allow to turn forall into some exists.– chi
Jan 11 at 14:05
I can't prove that either. At best, I can check that the analogous strategy fails. That encoding for "exists" is a consequence of Yoneda
T ~ (forall a. (T->a)->a) where we can take T = exists b. f b and exploit the type isomorphism (T->a) ~ (forall b. f b -> a), leading to the encoding above. The analogous strategy would be using co-Yoneda T ~ (exists a. a * (a -> T)), but here T is in positive (covariant) position, so choosing T ~ (forall b. f b) does not allow to turn forall into some exists.– chi
Jan 11 at 14:05
add a comment |
0
active
oldest
votes
Your Answer
StackExchange.ifUsing("editor", function () {
StackExchange.using("externalEditor", function () {
StackExchange.using("snippets", function () {
StackExchange.snippets.init();
});
});
}, "code-snippets");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "1"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53375769%2fencoding-universal-types-in-terms-of-existential-types%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
0
active
oldest
votes
0
active
oldest
votes
active
oldest
votes
active
oldest
votes
Thanks for contributing an answer to Stack Overflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53375769%2fencoding-universal-types-in-terms-of-existential-types%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
You might want to look into skolemization: en.wikipedia.org/wiki/Skolem_normal_form
– Juan Pablo Santos
Nov 19 '18 at 16:34
1
@JuanPabloSantos I fail to see the connection
– Agnishom Chattopadhyay
Nov 19 '18 at 16:41
I can't prove that either. At best, I can check that the analogous strategy fails. That encoding for "exists" is a consequence of Yoneda
T ~ (forall a. (T->a)->a)where we can takeT = exists b. f band exploit the type isomorphism(T->a) ~ (forall b. f b -> a), leading to the encoding above. The analogous strategy would be using co-YonedaT ~ (exists a. a * (a -> T)), but hereTis in positive (covariant) position, so choosingT ~ (forall b. f b)does not allow to turnforallinto someexists.– chi
Jan 11 at 14:05