Finding a “free theorem”
How do I derive the free theorem for the type:
data F a = C1 Nat | C2 Bool Nat a
where Nat
is simply data Nat = Z | S Nat
?
In principle, this can be answered by the Haskell 'free-theorems' package, but it's too elderly to compile under any GHC version I can reasonably install.
haskell free-theorem
add a comment |
How do I derive the free theorem for the type:
data F a = C1 Nat | C2 Bool Nat a
where Nat
is simply data Nat = Z | S Nat
?
In principle, this can be answered by the Haskell 'free-theorems' package, but it's too elderly to compile under any GHC version I can reasonably install.
haskell free-theorem
2
Free theorems are usually associated to polymorphic function types. Otherwise, IIRC, you get a trivial theorem, e.g.fmap f = fmap f
wherefmap :: (a->b)-> F a -> F b
is the functor instance.
– chi
Nov 17 '18 at 14:39
add a comment |
How do I derive the free theorem for the type:
data F a = C1 Nat | C2 Bool Nat a
where Nat
is simply data Nat = Z | S Nat
?
In principle, this can be answered by the Haskell 'free-theorems' package, but it's too elderly to compile under any GHC version I can reasonably install.
haskell free-theorem
How do I derive the free theorem for the type:
data F a = C1 Nat | C2 Bool Nat a
where Nat
is simply data Nat = Z | S Nat
?
In principle, this can be answered by the Haskell 'free-theorems' package, but it's too elderly to compile under any GHC version I can reasonably install.
haskell free-theorem
haskell free-theorem
asked Nov 17 '18 at 13:58
NietzscheanAINietzscheanAI
431415
431415
2
Free theorems are usually associated to polymorphic function types. Otherwise, IIRC, you get a trivial theorem, e.g.fmap f = fmap f
wherefmap :: (a->b)-> F a -> F b
is the functor instance.
– chi
Nov 17 '18 at 14:39
add a comment |
2
Free theorems are usually associated to polymorphic function types. Otherwise, IIRC, you get a trivial theorem, e.g.fmap f = fmap f
wherefmap :: (a->b)-> F a -> F b
is the functor instance.
– chi
Nov 17 '18 at 14:39
2
2
Free theorems are usually associated to polymorphic function types. Otherwise, IIRC, you get a trivial theorem, e.g.
fmap f = fmap f
where fmap :: (a->b)-> F a -> F b
is the functor instance.– chi
Nov 17 '18 at 14:39
Free theorems are usually associated to polymorphic function types. Otherwise, IIRC, you get a trivial theorem, e.g.
fmap f = fmap f
where fmap :: (a->b)-> F a -> F b
is the functor instance.– chi
Nov 17 '18 at 14:39
add a comment |
1 Answer
1
active
oldest
votes
There is an online generator for free theorems at, and when it was down a little while ago I created an alternative UI that runs completely in the browser (using reflex-dom
).
But the deeper problem is that free theorems, in the sense of these packages, are properties of polymorphic functions, so in order to answer your question, you have to give a function (like map
) whose free theorem you are interested in.
add a comment |
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%2f53351894%2ffinding-a-free-theorem%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
There is an online generator for free theorems at, and when it was down a little while ago I created an alternative UI that runs completely in the browser (using reflex-dom
).
But the deeper problem is that free theorems, in the sense of these packages, are properties of polymorphic functions, so in order to answer your question, you have to give a function (like map
) whose free theorem you are interested in.
add a comment |
There is an online generator for free theorems at, and when it was down a little while ago I created an alternative UI that runs completely in the browser (using reflex-dom
).
But the deeper problem is that free theorems, in the sense of these packages, are properties of polymorphic functions, so in order to answer your question, you have to give a function (like map
) whose free theorem you are interested in.
add a comment |
There is an online generator for free theorems at, and when it was down a little while ago I created an alternative UI that runs completely in the browser (using reflex-dom
).
But the deeper problem is that free theorems, in the sense of these packages, are properties of polymorphic functions, so in order to answer your question, you have to give a function (like map
) whose free theorem you are interested in.
There is an online generator for free theorems at, and when it was down a little while ago I created an alternative UI that runs completely in the browser (using reflex-dom
).
But the deeper problem is that free theorems, in the sense of these packages, are properties of polymorphic functions, so in order to answer your question, you have to give a function (like map
) whose free theorem you are interested in.
answered Nov 17 '18 at 14:40
Joachim BreitnerJoachim Breitner
20.4k563110
20.4k563110
add a comment |
add a comment |
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%2f53351894%2ffinding-a-free-theorem%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
2
Free theorems are usually associated to polymorphic function types. Otherwise, IIRC, you get a trivial theorem, e.g.
fmap f = fmap f
wherefmap :: (a->b)-> F a -> F b
is the functor instance.– chi
Nov 17 '18 at 14:39