{"comment":{"created_at":"2011-10-22T05:01:11Z","body":"The \"C doesn't have an arrow in it\" approach is only sufficient for closed contracts.","updated_at":"2011-10-22T05:01:11Z","url":"https://api.github.com/repos/samth/var/issues/comments/2488459","id":2488459,"user":{"avatar_url":"https://secure.gravatar.com/avatar/49662e9a0b0a07a77a490b3d32b65d8e?d=https://a248.e.akamai.net/assets.github.com%2Fimages%2Fgravatars%2Fgravatar-140.png","gravatar_id":"49662e9a0b0a07a77a490b3d32b65d8e","url":"https://api.github.com/users/dvanhorn","id":205413,"login":"dvanhorn"}},"action":"created","issue":{"number":3,"created_at":"2011-10-20T00:41:34Z","pull_request":{"diff_url":null,"patch_url":null,"html_url":null},"body":"Here's a contract:\r\n\r\n```(rec/c X  (or/c (cons/c X X) (-> (pred string? †)))))```\r\n\r\nNotice that it is a legit contract according to our grammar -- productive and `FLAT` on the left and `HOC` on the right of the `or/c`.\r\n\r\nBut then\r\n\r\n```(unroll (rec/c X  (or/c (cons/c X X) (-> (pred string? †)))))```\r\n\r\nain't a contract because it's `HOC` on the left and right.  So unroll is not total.\r\n\r\nThe problem is that `X` is considered `FLAT`, which isn't right -- but it's not `HOC` either.  It really depends on the contract in which it's bound.  In this case, it's always `HOC`.  But imagine:\r\n\r\n```(rec/c X (or/c (cons/c X X) empty))```\r\n\r\nhere, `X` is always `FLAT`.\r\n\r\nHere's a program that demonstrates the bad unrolling.\r\n\r\n    #lang var\r\n    (module f racket \r\n      (require)\r\n      (define v\r\n        (cons (-- (λ () \"a\")) (-- (λ () \"b\"))))\r\n      (provide/contract \r\n       [v (rec/c X (or/c (cons/c X X) (-> string?)))]))\r\n     \r\n    (require 'f)\r\n    v\r\n\r\nwhich gives\r\n\r\n    subst/μ: codomain test failed for (or/c (cons/c (rec/c X (or/c (cons/c X X) (-> (pred string? f)))) (rec/c X (or/c (cons/c X X) (-> (pred string? f))))) (-> (pred string? f))), call was (subst/μ X (rec/c X (or/c (cons/c X X) (-> (pred string? f)))) (or/c (cons/c X X) (-> (pred string? f))))","comments":3,"title":"Unroll is not total, FLAT v HOC not right for rec/c","updated_at":"2011-10-22T05:01:11Z","url":"https://api.github.com/repos/samth/var/issues/3","id":2000262,"assignee":null,"milestone":null,"closed_at":null,"user":{"avatar_url":"https://secure.gravatar.com/avatar/49662e9a0b0a07a77a490b3d32b65d8e?d=https://a248.e.akamai.net/assets.github.com%2Fimages%2Fgravatars%2Fgravatar-140.png","gravatar_id":"49662e9a0b0a07a77a490b3d32b65d8e","url":"https://api.github.com/users/dvanhorn","id":205413,"login":"dvanhorn"},"html_url":"https://github.com/samth/var/issues/3","labels":[],"state":"open"},"legacy":{"issue_id":2000262,"comment_id":2488459}}