{"action":"closed","issue":{"url":"https://api.github.com/repos/epsilonz/shoggoth.rs/issues/32","labels_url":"https://api.github.com/repos/epsilonz/shoggoth.rs/issues/32/labels{/name}","comments_url":"https://api.github.com/repos/epsilonz/shoggoth.rs/issues/32/comments","events_url":"https://api.github.com/repos/epsilonz/shoggoth.rs/issues/32/events","html_url":"https://github.com/epsilonz/shoggoth.rs/issues/32","id":59313926,"number":32,"title":"Rework type-level numerics for efficiency","user":{"login":"freebroccolo","id":151197,"avatar_url":"https://avatars.githubusercontent.com/u/151197?v=3","gravatar_id":"","url":"https://api.github.com/users/freebroccolo","html_url":"https://github.com/freebroccolo","followers_url":"https://api.github.com/users/freebroccolo/followers","following_url":"https://api.github.com/users/freebroccolo/following{/other_user}","gists_url":"https://api.github.com/users/freebroccolo/gists{/gist_id}","starred_url":"https://api.github.com/users/freebroccolo/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/freebroccolo/subscriptions","organizations_url":"https://api.github.com/users/freebroccolo/orgs","repos_url":"https://api.github.com/users/freebroccolo/repos","events_url":"https://api.github.com/users/freebroccolo/events{/privacy}","received_events_url":"https://api.github.com/users/freebroccolo/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/epsilonz/shoggoth.rs/labels/B-clarifying","name":"B-clarifying","color":"e102d8"},{"url":"https://api.github.com/repos/epsilonz/shoggoth.rs/labels/E-hard","name":"E-hard","color":"02e10c"}],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-02-28T00:22:32Z","updated_at":"2015-05-12T15:50:14Z","closed_at":"2015-05-12T15:50:14Z","body":"The type-level numerics story has been slowly improving through the last several refactorings and with the current binary encoding it's efficient enough for some limited practical use. I have a working implementation of sized data structures that depends on it that I may release soon.\r\n\r\nHowever, the binary arithmetic is still probably not efficient enough for working with very large numbers or even large collections of smaller numbers. If we had an efficient enough representation, we could actually implement singleton encodings for most of the built in types already. `()`, `bool`, and other finite structures are trivial. The fixed precision numeric types like `u8`, …, `u64` can be represented using comparison bounds on `Nat`. We could even use `List` or the new `Diff` (defunctionalized difference `List`) for sequences, and represent `String` as sequences of reified bytes.\r\n\r\nIt should be possible to implement builtin support for efficient representations in Rust, similar to what `Agda` and `Idris` allow, but for now I'm assuming that's not going to happen, at least not anytime soon. There are a couple of alternatives though.\r\n\r\nOne thing we could try is to switch to type-level hexadecimal natural numbers. This should decrease representational and operational complexity at the expense of complexity on the implementation and code generation side. It would also be a huge pain to implement the operations manually, so we'd pretty much have to write some nice macros to parse tables of rules and fill in all the boilerplate. Somewhat surprisingly, I haven't been able to find many existing implementations of either type-level hexadecimal arithmetic or even just hexadecimal infinite precision natural numbers. Of course Kmett has a version though…\r\n\r\nThe hexadecimal approach would be an improvement and should be mostly straightforward, just extremely tedious. Given the required effort, I'm inclined to explore other more exotic alternatives first. Recently I've come across several possibilities involving arithmetic with compressed representations of natural numbers that seem to have very impressive complexity characteristics. Initially I was reluctant to pursue such possibilities because the representations would have been pretty hard for the user to work with. Type macros make the difference though I think. Ideally we would have pretty type errors too but if the macros RFC is accepted I'll submit something for that too."}}