{"action":"created","issue":{"url":"https://api.github.com/repos/lukstafi/invargent/issues/5","labels_url":"https://api.github.com/repos/lukstafi/invargent/issues/5/labels{/name}","comments_url":"https://api.github.com/repos/lukstafi/invargent/issues/5/comments","events_url":"https://api.github.com/repos/lukstafi/invargent/issues/5/events","html_url":"https://github.com/lukstafi/invargent/issues/5","id":66657228,"number":5,"title":"append (and flatten) List typing","user":{"login":"Drup","id":801124,"avatar_url":"https://avatars.githubusercontent.com/u/801124?v=3","gravatar_id":"","url":"https://api.github.com/users/Drup","html_url":"https://github.com/Drup","followers_url":"https://api.github.com/users/Drup/followers","following_url":"https://api.github.com/users/Drup/following{/other_user}","gists_url":"https://api.github.com/users/Drup/gists{/gist_id}","starred_url":"https://api.github.com/users/Drup/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Drup/subscriptions","organizations_url":"https://api.github.com/users/Drup/orgs","repos_url":"https://api.github.com/users/Drup/repos","events_url":"https://api.github.com/users/Drup/events{/privacy}","received_events_url":"https://api.github.com/users/Drup/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-04-06T17:17:47Z","updated_at":"2015-04-06T20:25:22Z","closed_at":"2015-04-06T17:55:18Z","body":"When I used the list type commonly defined in your examples: \r\n```\r\ndatatype List : type * num\r\ndatacons LNil : ∀a. List(a, 0)\r\ndatacons LCons : ∀n, a [0≤n]. a * List(a, n) ⟶ List(a, n+1)\r\n``` \r\nThe append function\r\n```\r\nlet rec append l1 l2 = match l1 with\r\n  | LNil -> l2\r\n  | LCons (h,t) -> LCons (h,append t l2)\r\n```\r\nget type \r\n```\r\n∀k, n, a[1 ≤ k + n ∧ 1 ≤ n].\r\n  List (a, k) → List (a, n) → List (a, n + k)\r\n```\r\nhowever, I don't see why the second list should have a length of at least one.\r\nI can \"fix\" it by removing the constraint in LCons: `datacons LCons : ∀n, a. a * List(a, n) ⟶ List(a, n+1)`.\r\n\r\nIf I define flatten:\r\n```\r\nlet rec flatten = function\r\n  | LNil -> LNil\r\n  | LCons (t, l) -> append t (flatten l)\r\n```\r\nThe original version get a timeout. The modified version get the rather uninteresting `∀n, a. List (List (a, 0), n) → List (a, 0)`."},"comment":{"url":"https://api.github.com/repos/lukstafi/invargent/issues/comments/90229830","html_url":"https://github.com/lukstafi/invargent/issues/5#issuecomment-90229830","issue_url":"https://api.github.com/repos/lukstafi/invargent/issues/5","id":90229830,"user":{"login":"Drup","id":801124,"avatar_url":"https://avatars.githubusercontent.com/u/801124?v=3","gravatar_id":"","url":"https://api.github.com/users/Drup","html_url":"https://github.com/Drup","followers_url":"https://api.github.com/users/Drup/followers","following_url":"https://api.github.com/users/Drup/following{/other_user}","gists_url":"https://api.github.com/users/Drup/gists{/gist_id}","starred_url":"https://api.github.com/users/Drup/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Drup/subscriptions","organizations_url":"https://api.github.com/users/Drup/orgs","repos_url":"https://api.github.com/users/Drup/repos","events_url":"https://api.github.com/users/Drup/events{/privacy}","received_events_url":"https://api.github.com/users/Drup/received_events","type":"User","site_admin":false},"created_at":"2015-04-06T20:25:22Z","updated_at":"2015-04-06T20:25:22Z","body":"> `val flatten : ∀k, n, a[0 ≤ n]. List (List (a, n), k) → ∃n[0 ≤ n].List (a, n)`\r\n\r\ninvargent can't infer k * n ?"}}