{"action":"created","issue":{"url":"https://api.github.com/repos/Gabriel439/Haskell-Morte-Library/issues/30","repository_url":"https://api.github.com/repos/Gabriel439/Haskell-Morte-Library","labels_url":"https://api.github.com/repos/Gabriel439/Haskell-Morte-Library/issues/30/labels{/name}","comments_url":"https://api.github.com/repos/Gabriel439/Haskell-Morte-Library/issues/30/comments","events_url":"https://api.github.com/repos/Gabriel439/Haskell-Morte-Library/issues/30/events","html_url":"https://github.com/Gabriel439/Haskell-Morte-Library/issues/30","id":118197964,"number":30,"title":"Should we add Self types?","user":{"login":"MaiaVictor","id":13090166,"avatar_url":"https://avatars.githubusercontent.com/u/13090166?v=3","gravatar_id":"","url":"https://api.github.com/users/MaiaVictor","html_url":"https://github.com/MaiaVictor","followers_url":"https://api.github.com/users/MaiaVictor/followers","following_url":"https://api.github.com/users/MaiaVictor/following{/other_user}","gists_url":"https://api.github.com/users/MaiaVictor/gists{/gist_id}","starred_url":"https://api.github.com/users/MaiaVictor/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/MaiaVictor/subscriptions","organizations_url":"https://api.github.com/users/MaiaVictor/orgs","repos_url":"https://api.github.com/users/MaiaVictor/repos","events_url":"https://api.github.com/users/MaiaVictor/events{/privacy}","received_events_url":"https://api.github.com/users/MaiaVictor/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":23,"created_at":"2015-11-21T13:53:41Z","updated_at":"2016-03-22T20:38:08Z","closed_at":null,"body":"The Scott encoding is an important tool that is ultimately necessary for many efficient algorithms on the untyped lambda calculus. It is impossible to encode Scott encoded values on Morte. Things such as `zipWith` and `min` are quadratic. [Self Types](http://homepage.cs.uiowa.edu/~astump/papers/fu-stump-rta-tlca-14.pdf) enable the Scott Encoding, and linear zipWith/min/similar functions without compromising strongly normalization or soundness. The extension is so simple it could be added in Morte as it is as a few lines of code.\r\n\r\nI could submit a pull request if Gabriel wishes. Should Self types be added?"},"comment":{"url":"https://api.github.com/repos/Gabriel439/Haskell-Morte-Library/issues/comments/200011178","html_url":"https://github.com/Gabriel439/Haskell-Morte-Library/issues/30#issuecomment-200011178","issue_url":"https://api.github.com/repos/Gabriel439/Haskell-Morte-Library/issues/30","id":200011178,"user":{"login":"MaiaVictor","id":13090166,"avatar_url":"https://avatars.githubusercontent.com/u/13090166?v=3","gravatar_id":"","url":"https://api.github.com/users/MaiaVictor","html_url":"https://github.com/MaiaVictor","followers_url":"https://api.github.com/users/MaiaVictor/followers","following_url":"https://api.github.com/users/MaiaVictor/following{/other_user}","gists_url":"https://api.github.com/users/MaiaVictor/gists{/gist_id}","starred_url":"https://api.github.com/users/MaiaVictor/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/MaiaVictor/subscriptions","organizations_url":"https://api.github.com/users/MaiaVictor/orgs","repos_url":"https://api.github.com/users/MaiaVictor/repos","events_url":"https://api.github.com/users/MaiaVictor/events{/privacy}","received_events_url":"https://api.github.com/users/MaiaVictor/received_events","type":"User","site_admin":false},"created_at":"2016-03-22T20:38:08Z","updated_at":"2016-03-22T20:38:08Z","body":"@ChristopherKing42 I don't visualize how that would work. Can we try with a concrete example?\r\n\r\n    -- ∀ a . a -> ChurchNat -> ChurchList a -> a\r\n    get_at index default list = (list cons nil scott_nat) \r\n        \r\n        -- a -> ScottList a -> ChurchNat -> a\r\n        cons head tail nat = (nat Succ? Zero?)\r\n            Succ? pred = (tail pred)\r\n            Zero?      = head\r\n\r\n        -- ChurchNat -> a\r\n        nil nat = default\r\n        \r\n        -- ScottNat\r\n        scott_nat = (index Succ Zero)\r\n            Succ pred = (Succ Zero -> (Succ pred))\r\n            Zero      = (Succ Zero -> Zero)\r\n\r\nThis function takes an church-encoded nat (`index`), a `default` value, and a church-encoded `list`, and returns the element at that index, or `default` if the `index` is out of bound. Since this function involves the inspection of two recursive datatypes (list and nat), I needed to convert one of them (the nat) to scott in order to avoid O(N^2) complexity.\r\n\r\nCould you show me how would work on Morte?\r\n\r\n\r\n\r\n    -- ∀ a b . (a -> b) -> ChurchList a -> ChurchList b\r\n    map fn list = (cons nil -> (list cons? nil?))\r\n        cons? head tail = (cons (fn head) tail)\r\n        nil?            = nil\r\n\r\n    -- ∀ a . a -> ChurchNat -> ChurchList a -> a\r\n    get_at index default list = (head (index tail scott_list))\r\n        \r\n        ---- :: ScottList a -> a\r\n        head list = (list Cons? Nil?)\r\n            Cons? head tail = head\r\n            Nil?            = default\r\n\r\n        ---- :: ScottList a -> ScottList a\r\n        tail list = (list Cons? Nil?)\r\n            Cons? head tail = tail\r\n            Nil?            = (Cons Nil -> (Cons default Nil))\r\n\r\n        -- :: ScottList a\r\n        scott_list = (list Cons Nil)\r\n            Cons head tail = (Cons Nil -> (Cons head tail))\r\n            Nil            = (Cons Nil -> Nil)\r\n\r\nThere are two functions here. `map`, which is what you're used to, and works on Church-encoded data. There is `get_at`, which takes an `index`, a `default` value, a `list` (Church-encoded), and returns the element at position `index`, or `default` if `index` is out of range.\r\n\r\nWhat is interesting about the `get_at` function? It involves some kind of recursive run through two structures: a list and a natural number. Remember you can't use recursion - we are using folds for where we would use recursion on Haskell. In that case, you need to chose one of the two structures - the list or the nat - to fuel the recursion with its fold. But when you make that choice, you already got the recursion going on. If you chose the list, you can't access the inner structure of the `nat` **without kicking its recursion**, because that's how church works. If you chose the nat, you can't access the elements of the list. If you do, you kick its recursion and then you get quadratic time.\r\n\r\nSo, what is the solution? Simple: you scott-encode one of the structures and pass it to the church-encoded one. That is how `get_at` works: it scott encodes the list and sends it to the nat. And, by doing so, you don't gain just \r\n\r\n"}}