Finding a “free theorem”












2















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.










share|improve this question


















  • 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
















2















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.










share|improve this question


















  • 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














2












2








2


1






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.










share|improve this question














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






share|improve this question













share|improve this question











share|improve this question




share|improve this question










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 where fmap :: (a->b)-> F a -> F b is the functor instance.

    – chi
    Nov 17 '18 at 14:39














  • 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








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












1 Answer
1






active

oldest

votes


















4














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.






share|improve this answer























    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
    });


    }
    });














    draft saved

    draft discarded


















    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









    4














    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.






    share|improve this answer




























      4














      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.






      share|improve this answer


























        4












        4








        4







        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.






        share|improve this answer













        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.







        share|improve this answer












        share|improve this answer



        share|improve this answer










        answered Nov 17 '18 at 14:40









        Joachim BreitnerJoachim Breitner

        20.4k563110




        20.4k563110






























            draft saved

            draft discarded




















































            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.




            draft saved


            draft discarded














            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





















































            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







            Popular posts from this blog

            Guess what letter conforming each word

            Port of Spain

            Run scheduled task as local user group (not BUILTIN)