{"action":"created","issue":{"url":"https://api.github.com/repos/dhall-lang/dhall-haskell/issues/291","repository_url":"https://api.github.com/repos/dhall-lang/dhall-haskell","labels_url":"https://api.github.com/repos/dhall-lang/dhall-haskell/issues/291/labels{/name}","comments_url":"https://api.github.com/repos/dhall-lang/dhall-haskell/issues/291/comments","events_url":"https://api.github.com/repos/dhall-lang/dhall-haskell/issues/291/events","html_url":"https://github.com/dhall-lang/dhall-haskell/issues/291","id":298608735,"number":291,"title":"Normalization for Optional/build doesn't always match semantics","user":{"login":"ocharles","id":20878,"avatar_url":"https://avatars2.githubusercontent.com/u/20878?v=4","gravatar_id":"","url":"https://api.github.com/users/ocharles","html_url":"https://github.com/ocharles","followers_url":"https://api.github.com/users/ocharles/followers","following_url":"https://api.github.com/users/ocharles/following{/other_user}","gists_url":"https://api.github.com/users/ocharles/gists{/gist_id}","starred_url":"https://api.github.com/users/ocharles/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ocharles/subscriptions","organizations_url":"https://api.github.com/users/ocharles/orgs","repos_url":"https://api.github.com/users/ocharles/repos","events_url":"https://api.github.com/users/ocharles/events{/privacy}","received_events_url":"https://api.github.com/users/ocharles/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-02-20T14:14:47Z","updated_at":"2018-02-20T14:19:14Z","closed_at":null,"author_association":"COLLABORATOR","body":"I may be understanding something wrong, but I'm implementing\r\n\r\n```\r\nf ⇥ Optional/build A\r\ng (Optional A) (λ(a : A) → [ a ] : Optional A) ([] : Optional A) ⇥ b\r\n────────────────────────────────────────────────────────────────────\r\nf g ⇥ b\r\n```\r\n\r\nThe tests for this project show (in `normalization/optionalBuildA` and `normalization/optionalBuildB`) that\r\n\r\n```\r\n      λ(id : ∀(a : Type) → a → a)\r\n    → Optional/build\r\n      Bool\r\n      (   λ(optional : Type)\r\n        → λ(just : Bool → optional)\r\n        → λ(nothing : optional)\r\n        → id optional (just True)\r\n      )\r\n```\r\n\r\nshould reduce to\r\n\r\n```\r\n      λ(id : ∀(a : Type) → a → a)\r\n    → Optional/build\r\n      Bool\r\n      (   λ(optional : Type)\r\n        → λ(just : Bool → optional)\r\n        → λ(nothing : optional)\r\n        → id optional (just True)\r\n      )\r\n```\r\n\r\nHowever, my implementation of the rule shows that it actually reduces to\r\n\r\n```\r\nλ(id : ∀(a : Type) → a → a) → id (Optional Bool) ([ True ] : Optional Bool)\r\n```\r\n\r\nI believe this is correct, as we can do this in `dhall`:\r\n\r\n```\r\n[nix-shell:~/work/dhall.js]$ dhall\r\n\\ ( id : forall ( a : Type ) -> a -> a ) ->\r\nlet A : Type = Bool in\r\nlet g = \r\n      (   λ(optional : Type)\r\n        → λ(just : Bool → optional)\r\n        → λ(nothing : optional)\r\n        → id optional (just True)\r\n      )\r\nin g (Optional A) (λ(a : A) → [ a ] : Optional A) ([] : Optional A)\r\n\r\n∀(id : ∀(a : Type) → a → a) → Optional Bool\r\n\r\nλ(id : ∀(a : Type) → a → a) → id (Optional Bool) ([ True ] : Optional Bool)\r\n```\r\n\r\nHere I've bought `A` and `g` into scope with `let`. I know that `f ⇥ Optional/build A` holds, so I need to know what `b` is in `g (Optional A) (λ(a : A) → [ a ] : Optional A) ([] : Optional A) ⇥ b` - the above shows me it's just `id (Optional Bool) ([ True ] : Optional Bool)`.\r\n\r\n`dhall.js` has this normalization behavior, but causes it to fail tests."},"comment":{"url":"https://api.github.com/repos/dhall-lang/dhall-haskell/issues/comments/366991126","html_url":"https://github.com/dhall-lang/dhall-haskell/issues/291#issuecomment-366991126","issue_url":"https://api.github.com/repos/dhall-lang/dhall-haskell/issues/291","id":366991126,"user":{"login":"ocharles","id":20878,"avatar_url":"https://avatars2.githubusercontent.com/u/20878?v=4","gravatar_id":"","url":"https://api.github.com/users/ocharles","html_url":"https://github.com/ocharles","followers_url":"https://api.github.com/users/ocharles/followers","following_url":"https://api.github.com/users/ocharles/following{/other_user}","gists_url":"https://api.github.com/users/ocharles/gists{/gist_id}","starred_url":"https://api.github.com/users/ocharles/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ocharles/subscriptions","organizations_url":"https://api.github.com/users/ocharles/orgs","repos_url":"https://api.github.com/users/ocharles/repos","events_url":"https://api.github.com/users/ocharles/events{/privacy}","received_events_url":"https://api.github.com/users/ocharles/received_events","type":"User","site_admin":false},"created_at":"2018-02-20T14:19:14Z","updated_at":"2018-02-20T14:19:14Z","author_association":"COLLABORATOR","body":"Removing `id` does cause normalization:\r\n\r\n```\r\nOptional/build\r\n      Bool\r\n      (   λ(optional : Type)\r\n        → λ(just : Bool → optional)\r\n        → λ(nothing : optional)\r\n        → just True\r\n      )\r\nOptional Bool\r\n\r\n[ True ] : Optional Bool\r\n```\r\n\r\nI don't see why the presence of `id` should change things. Am I missing something?"}}
{"actor":{"display_login":"ocharles"}}