{"action":"created","issue":{"url":"https://api.github.com/repos/TheSeamau5/elm-check/issues/3","labels_url":"https://api.github.com/repos/TheSeamau5/elm-check/issues/3/labels{/name}","comments_url":"https://api.github.com/repos/TheSeamau5/elm-check/issues/3/comments","events_url":"https://api.github.com/repos/TheSeamau5/elm-check/issues/3/events","html_url":"https://github.com/TheSeamau5/elm-check/issues/3","id":72051467,"number":3,"title":"Playing the Applicative Game with Claims and Proofs","user":{"login":"TheSeamau5","id":3227869,"avatar_url":"https://avatars.githubusercontent.com/u/3227869?v=3","gravatar_id":"","url":"https://api.github.com/users/TheSeamau5","html_url":"https://github.com/TheSeamau5","followers_url":"https://api.github.com/users/TheSeamau5/followers","following_url":"https://api.github.com/users/TheSeamau5/following{/other_user}","gists_url":"https://api.github.com/users/TheSeamau5/gists{/gist_id}","starred_url":"https://api.github.com/users/TheSeamau5/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/TheSeamau5/subscriptions","organizations_url":"https://api.github.com/users/TheSeamau5/orgs","repos_url":"https://api.github.com/users/TheSeamau5/repos","events_url":"https://api.github.com/users/TheSeamau5/events{/privacy}","received_events_url":"https://api.github.com/users/TheSeamau5/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/TheSeamau5/elm-check/labels/enhancement","name":"enhancement","color":"84b6eb"}],"state":"open","locked":false,"assignee":{"login":"TheSeamau5","id":3227869,"avatar_url":"https://avatars.githubusercontent.com/u/3227869?v=3","gravatar_id":"","url":"https://api.github.com/users/TheSeamau5","html_url":"https://github.com/TheSeamau5","followers_url":"https://api.github.com/users/TheSeamau5/followers","following_url":"https://api.github.com/users/TheSeamau5/following{/other_user}","gists_url":"https://api.github.com/users/TheSeamau5/gists{/gist_id}","starred_url":"https://api.github.com/users/TheSeamau5/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/TheSeamau5/subscriptions","organizations_url":"https://api.github.com/users/TheSeamau5/orgs","repos_url":"https://api.github.com/users/TheSeamau5/repos","events_url":"https://api.github.com/users/TheSeamau5/events{/privacy}","received_events_url":"https://api.github.com/users/TheSeamau5/received_events","type":"User","site_admin":false},"milestone":{"url":"https://api.github.com/repos/TheSeamau5/elm-check/milestones/1","html_url":"https://github.com/TheSeamau5/elm-check/milestones/0.15","labels_url":"https://api.github.com/repos/TheSeamau5/elm-check/milestones/1/labels","id":1093662,"number":1,"title":"0.15","description":"Get elm-check ready for 0.15\r\n\r\nFeatures that will be included:\r\n\r\n- Shrinking\r\n- JSON decoding and encoding of test results\r\n- elm-test integration\r\n- Continuous local testing\r\n- Simple HTML test runner\r\n- Optional User-friendly DSL\r\n- Simplified terminology\r\n- Tutorials and wikis\r\n- A big example","creator":{"login":"TheSeamau5","id":3227869,"avatar_url":"https://avatars.githubusercontent.com/u/3227869?v=3","gravatar_id":"","url":"https://api.github.com/users/TheSeamau5","html_url":"https://github.com/TheSeamau5","followers_url":"https://api.github.com/users/TheSeamau5/followers","following_url":"https://api.github.com/users/TheSeamau5/following{/other_user}","gists_url":"https://api.github.com/users/TheSeamau5/gists{/gist_id}","starred_url":"https://api.github.com/users/TheSeamau5/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/TheSeamau5/subscriptions","organizations_url":"https://api.github.com/users/TheSeamau5/orgs","repos_url":"https://api.github.com/users/TheSeamau5/repos","events_url":"https://api.github.com/users/TheSeamau5/events{/privacy}","received_events_url":"https://api.github.com/users/TheSeamau5/received_events","type":"User","site_admin":false},"open_issues":2,"closed_issues":1,"state":"open","created_at":"2015-05-02T20:59:42Z","updated_at":"2015-05-02T21:01:18Z","due_on":null,"closed_at":null},"comments":8,"created_at":"2015-04-30T03:30:39Z","updated_at":"2015-05-03T01:29:19Z","closed_at":null,"body":"So, I open this issue to not clobber https://github.com/TheSeamau5/elm-check/issues/2.\r\n\r\nI've explored a bit the idea of using \"claims\" and \"proofs\" as the way of exposing a friendly DSL-y interface for the user a-la https://github.com/TheSeamau5/elm-check/pull/1 by @sgraf812\r\n\r\nThe idea is as follows. You make \"claims\" about your system like the fact that reversing a list twice should yield the original list.\r\n\r\nIn code, this would look something like this:\r\n\r\n```elm\r\nclaim_reverse_involution =\r\n  claim\r\n    \"Reversing a list twice yields the original list\"\r\n  `that`\r\n    List.reverse >> List.reverse\r\n  `equals`\r\n    identity\r\n```\r\n\r\nNow, this is just a claim about any list. Unlike normally with `elm-check`, this doesn't get tied up to a particular type, which conceptually seperates the claim from the actual trying to prove or find a counter example.\r\n\r\nSo, suppose we believe that this \"claim\" should be true, we can tell `elm-check` to \"prove\" it for some given input space.\r\n\r\n```elm\r\nproof_reverse_involution =\r\n  prove\r\n    claim_reverse_involution\r\n  `for`\r\n    list int\r\n```\r\n\r\nNow, what we get is a proof, which is equivalent to the old `Property` type where this is just `Int -> Seed -> TestResult`\r\n\r\nIf instead you wish to \"disprove\" the claim, you can just use `disprove` instead of `prove` and that'll just flip the expected `Bool` value\r\n\r\n```elm\r\ncounter_reverse_involution = \r\n  disprove\r\n    claim_reverse_involution\r\n  `for`\r\n    list int\r\n```\r\n\r\nAnd, now, when you actually want to run these things, you can call `check`, which as a word makes sense in this context because you want to \"check\" proofs and \"check\" for counter examples.\r\n\r\n```elm\r\ncheck proof_reverse_induction\r\n```\r\n\r\nand this will give you the actual `TestResult` (modulo seeds and number of runs).\r\n\r\nAny opinions, @evancz ? Does this terminology seem to make more sense in this context ?"},"comment":{"url":"https://api.github.com/repos/TheSeamau5/elm-check/issues/comments/98424078","html_url":"https://github.com/TheSeamau5/elm-check/issues/3#issuecomment-98424078","issue_url":"https://api.github.com/repos/TheSeamau5/elm-check/issues/3","id":98424078,"user":{"login":"TheSeamau5","id":3227869,"avatar_url":"https://avatars.githubusercontent.com/u/3227869?v=3","gravatar_id":"","url":"https://api.github.com/users/TheSeamau5","html_url":"https://github.com/TheSeamau5","followers_url":"https://api.github.com/users/TheSeamau5/followers","following_url":"https://api.github.com/users/TheSeamau5/following{/other_user}","gists_url":"https://api.github.com/users/TheSeamau5/gists{/gist_id}","starred_url":"https://api.github.com/users/TheSeamau5/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/TheSeamau5/subscriptions","organizations_url":"https://api.github.com/users/TheSeamau5/orgs","repos_url":"https://api.github.com/users/TheSeamau5/repos","events_url":"https://api.github.com/users/TheSeamau5/events{/privacy}","received_events_url":"https://api.github.com/users/TheSeamau5/received_events","type":"User","site_admin":false},"created_at":"2015-05-03T01:29:18Z","updated_at":"2015-05-03T01:29:18Z","body":"So, I just got a bit of a reality check when I worked on the DSL. Turns out that it needs slight tweaks to be able to work with the type system. Basically, if you have multi-arity functions, you need to work with tuples explicitly for it to work, which is not that big of a deal, to be honest.\r\n\r\nThis is how the example would look:\r\n\r\n```elm\r\nclaim_reverse_append =   \r\n  claim \r\n    \"Appending then reversing lists is equivalent to reversing then appending\"\r\n  `that`\r\n    (\\(l1, l2) -> List.reverse (l1 ++ l2))\r\n  `is`\r\n    (\\(l1, l2) -> List.reverse l1 ++ List.reverse l2)\r\n  `for`\r\n    tuple (list int, list int)\r\n```\r\n\r\nGood news is that I can even offer this:\r\n\r\n```elm\r\nclaim_length_list_positive = \r\n  claim\r\n    \"Length of a list is always positive\"\r\n  `true`\r\n    (\\list -> List.length list > 0)\r\n  `for`\r\n    list int\r\n```\r\n\r\nSo, you can claim things to be `true` or `false` pretty easily. And, `claim` is the same exact `claim` function as defined in `Check.elm`. There's no fancy builder business. It's just, straight up interspersing the code with words that just pass on the next thing to the previous thing. This means the DSL is pretty transparent and is just there to help readability. "}}