{"action":"created","issue":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2670","labels_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2670/labels{/name}","comments_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2670/comments","events_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2670/events","html_url":"https://github.com/idris-lang/Idris-dev/issues/2670","id":108492928,"number":2670,"title":"Module names should be required to match filenames.","user":{"login":"cbiffle","id":45247,"avatar_url":"https://avatars.githubusercontent.com/u/45247?v=3","gravatar_id":"","url":"https://api.github.com/users/cbiffle","html_url":"https://github.com/cbiffle","followers_url":"https://api.github.com/users/cbiffle/followers","following_url":"https://api.github.com/users/cbiffle/following{/other_user}","gists_url":"https://api.github.com/users/cbiffle/gists{/gist_id}","starred_url":"https://api.github.com/users/cbiffle/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cbiffle/subscriptions","organizations_url":"https://api.github.com/users/cbiffle/orgs","repos_url":"https://api.github.com/users/cbiffle/repos","events_url":"https://api.github.com/users/cbiffle/events{/privacy}","received_events_url":"https://api.github.com/users/cbiffle/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":3,"created_at":"2015-09-26T20:09:43Z","updated_at":"2015-09-28T16:56:22Z","closed_at":null,"body":"Currently, imports work in terms of file paths, but qualified references work in terms of module names.  The two have no relation.\r\n\r\nAs an example, consider these two files:\r\n\r\n**Foo.idr**\r\n```idris\r\nmodule Bar\r\n\r\nvalue : Nat\r\nvalue = 3\r\n```\r\n\r\n**Bar.idr**\r\n```idris\r\nmodule Foo\r\n\r\nvalue : Nat\r\nvalue = 4\r\n```\r\n\r\nNow consider the use of these modules:\r\n\r\n```idris\r\nimport Foo  -- imports module \"Bar\"\r\nimport Bar  -- imports module \"Foo\"\r\n\r\nnewValue : Nat\r\nnewValue = Foo.value\r\n```\r\n\r\nWhat is the value of `Foo.value`?  It is 4.\r\n\r\nWhile this may seem somewhat contrived, I've run into this when rearranging a codebase.  It's easy to `git mv` some files (possibly even permuting their names) and forget to update the `module` declarations.\r\n\r\nClearly, `import` must follow the filesystem; to do otherwise would require e.g. maintaining a database of which modules live where.\r\n\r\nI suggest that the behavior of `import` be preserved, but the compiler reject with an error any file that\r\n\r\n1. Contains a `module` declaration, and\r\n2. Resides at a path, from the root used by `import`, that doesn't match its module name, per the usual dot-for-separator substitution.\r\n\r\nPrecedent in existing languages (Java, Rust, Haskell) suggests that such a requirement is unlikely to be onerous."},"comment":{"url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/comments/143803688","html_url":"https://github.com/idris-lang/Idris-dev/issues/2670#issuecomment-143803688","issue_url":"https://api.github.com/repos/idris-lang/Idris-dev/issues/2670","id":143803688,"user":{"login":"nicolabotta","id":2726946,"avatar_url":"https://avatars.githubusercontent.com/u/2726946?v=3","gravatar_id":"","url":"https://api.github.com/users/nicolabotta","html_url":"https://github.com/nicolabotta","followers_url":"https://api.github.com/users/nicolabotta/followers","following_url":"https://api.github.com/users/nicolabotta/following{/other_user}","gists_url":"https://api.github.com/users/nicolabotta/gists{/gist_id}","starred_url":"https://api.github.com/users/nicolabotta/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nicolabotta/subscriptions","organizations_url":"https://api.github.com/users/nicolabotta/orgs","repos_url":"https://api.github.com/users/nicolabotta/repos","events_url":"https://api.github.com/users/nicolabotta/events{/privacy}","received_events_url":"https://api.github.com/users/nicolabotta/received_events","type":"User","site_admin":false},"created_at":"2015-09-28T16:56:22Z","updated_at":"2015-09-28T16:56:22Z","body":"If one accepts the idea that file names should match module names (which I do), why do we need the `module` keyword at all? The argument of the `import` command could just be a file name. No need for \"modules\", no confusion because of examples like the one above. "}}