Mixing
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 Chattopadhyay
824920
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 Chattopadhyay
824920
You might want to look into skolemization: en.wikipedia.org/wiki/Skolem_normal_form
– Juan Pablo Santos
Nov 19 '18 at 16:34
@JuanPabloSantos I fail to see the connection
– Agnishom Chattopadhyay
Nov 19 '18 at 16:41
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 Chattopadhyay
824920
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 Chattopadhyay
824920
asked Nov 19 '18 at 13:33
Agnishom Chattopadhyay
824920
edited Nov 19 '18 at 16:40
asked Nov 19 '18 at 13:33
Agnishom Chattopadhyay
824920
asked Nov 19 '18 at 13:33
Agnishom Chattopadhyay
824920
asked Nov 19 '18 at 13:33
Agnishom Chattopadhyay
824920
824920
You might want to look into skolemization: en.wikipedia.org/wiki/Skolem_normal_form
– Juan Pablo Santos
Nov 19 '18 at 16:34
@JuanPabloSantos I fail to see the connection
– Agnishom Chattopadhyay
Nov 19 '18 at 16:41
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
@JuanPabloSantos I fail to see the connection
– Agnishom Chattopadhyay
Nov 19 '18 at 16:41
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
@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
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.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- 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
@JuanPabloSantos I fail to see the connection
– Agnishom Chattopadhyay
Nov 19 '18 at 16:41