Name | inductive JSON |
Version |
0.0.1.post1
JSON |
| download |
home_page | None |
Summary | Inductive data structures for Python |
upload_time | 2024-12-06 07:46:24 |
maintainer | None |
docs_url | None |
author | None |
requires_python | >=3.12 |
license | MIT License Copyright (c) 2024 Qexat Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. |
keywords |
inductive
data structures
nat
natural numbers
list
linked list
dependent typing
|
VCS |
|
bugtrack_url |
|
requirements |
No requirements were recorded.
|
Travis-CI |
No Travis.
|
coveralls test coverage |
No coveralls.
|
# inductive
`inductive` is a Python library that defines inductive data structures such as Peano numbers and linked lists.
> [!CAUTION]
> It is still in early development.
## A missing puzzle piece
Despite being very useful, Python does not have a [built-in unsigned integer data type](https://docs.python.org/3/library/stdtypes.html#numeric-types-int-float-complex). Futhermore, it does not provide the ability to refine the existing `int` type by disallowing negative numbers - at least, not in a way that static type checkers like [`mypy`](https://mypy-lang.org/) or [`pyright`](https://microsoft.github.io/pyright/) can pick up.
And yet, natural numbers come up on many occasions, such as counting or ordering, or in mundane programming tasks.
>[!TIP]
> If you have ever created your own sequence type, and defined `__len__`, you are probably aware that you get a runtime error if it returns an integer below 0.
Fortunately for us, over the years, the language's type system [has become powerful enough](https://docs.python.org/3/reference/simple_stmts.html#type) to be able to encode [inductive types](https://en.wikipedia.org/wiki/Inductive_type).
### Inductive types
The idea goes as following: you start from *something*, like a pink ball - in our case, the number 0 - to which you add a box where you can put the ball, or another box of the same kind - for natural numbers, this is the [successor function](https://en.wikipedia.org/wiki/Successor_function). Then, you put the ball in a box, which itself is inside another box, and so on: you now have a number. What is its value? Simply count how many boxes you need to open to get to the ball.
![A pink ball surrounded by three boxes. The whole setup corresponds to the number 3.](./assets/boxes_and_balls_nat.png)
> Temporary mouse-drawn thingy until I find a better analogy 😆
Another way to think of it (and maybe even a better one!) is through [recursive functions](https://en.wikipedia.org/wiki/Recursion_(computer_science)), except that instead of returning values, it creates inhabitants of the type in a way that can understood statically.
## What does it give us?
This way, we are able to represent natural numbers in a type-safe way! If a value is of type `Nat`, you know it cannot be negative, which is sometimes a nice guarantee to have [as aforementioned](#a-missing-puzzle-piece). Also, this is very similar to the [Peano axioms](https://en.wikipedia.org/wiki/Peano_axioms), which gives us very nice mathematical properties.
However, this does not come without sacrificing some practicality: there is, as of writing this, no way to make the numeric literals have the type `Nat` instead of the built-in `int`. We still enjoy operators such as `+` or `*` thanks to their [corresponding magic methods](https://docs.python.org/3/reference/datamodel.html#emulating-numeric-types), but we will have to use functions to convert literals to our natural number type.
## But why stop here?
...We don't!
With the `type` statement added in Python 3.12 and structural pattern matching with `match`/`case` in 3.10, the language unlocked a lot of power at the type level. The latter, especially, is the best friend of inductive types ; and `Nat` is not the only one that is very useful!
Especially, I'm looking forward adding linked lists, inductive sets, trees, other numeric types that fit very well this little world.
>[!IMPORTANT]
> For now, only `Nat` is implemented, but it's just a matter of time before the others get added too 😄
`inductive` also provides a submodule `builtins` which goal is to override existing built-ins to use better suited types: for example, `len` is replaced by `length`, which returns a `Nat`, more appropriated since `len` can never return a negative number.
## Where does this idea come from?
More specifically, this library is heavily inspired by the proof assistant [Rocq](https://en.wikipedia.org/wiki/Coq_(software)) (previously known as Coq) and its programming language Gallina, which are based on a type theory called [calculus of constructions](https://en.wikipedia.org/wiki/Calculus_of_constructions), and more recently on its variant called [PCUIC](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.29) (predicative calculus of cumulative inductive constructions).
Raw data
{
"_id": null,
"home_page": null,
"name": "inductive",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.12",
"maintainer_email": null,
"keywords": "inductive, data structures, nat, natural numbers, list, linked list, dependent typing",
"author": null,
"author_email": "Lexa <contact@qexat.com>",
"download_url": "https://files.pythonhosted.org/packages/6c/35/91163c832e010772064dd6c9d67952f2e185e1aec895e5512dbf33cca865/inductive-0.0.1.post1.tar.gz",
"platform": null,
"description": "# inductive\n\n`inductive` is a Python library that defines inductive data structures such as Peano numbers and linked lists.\n\n> [!CAUTION]\n> It is still in early development.\n\n## A missing puzzle piece\n\nDespite being very useful, Python does not have a [built-in unsigned integer data type](https://docs.python.org/3/library/stdtypes.html#numeric-types-int-float-complex). Futhermore, it does not provide the ability to refine the existing `int` type by disallowing negative numbers - at least, not in a way that static type checkers like [`mypy`](https://mypy-lang.org/) or [`pyright`](https://microsoft.github.io/pyright/) can pick up.\nAnd yet, natural numbers come up on many occasions, such as counting or ordering, or in mundane programming tasks.\n\n>[!TIP]\n> If you have ever created your own sequence type, and defined `__len__`, you are probably aware that you get a runtime error if it returns an integer below 0.\n\nFortunately for us, over the years, the language's type system [has become powerful enough](https://docs.python.org/3/reference/simple_stmts.html#type) to be able to encode [inductive types](https://en.wikipedia.org/wiki/Inductive_type).\n\n### Inductive types\n\nThe idea goes as following: you start from *something*, like a pink ball - in our case, the number 0 - to which you add a box where you can put the ball, or another box of the same kind - for natural numbers, this is the [successor function](https://en.wikipedia.org/wiki/Successor_function). Then, you put the ball in a box, which itself is inside another box, and so on: you now have a number. What is its value? Simply count how many boxes you need to open to get to the ball.\n\n![A pink ball surrounded by three boxes. The whole setup corresponds to the number 3.](./assets/boxes_and_balls_nat.png)\n\n> Temporary mouse-drawn thingy until I find a better analogy \ud83d\ude06\n\nAnother way to think of it (and maybe even a better one!) is through [recursive functions](https://en.wikipedia.org/wiki/Recursion_(computer_science)), except that instead of returning values, it creates inhabitants of the type in a way that can understood statically.\n\n## What does it give us?\n\nThis way, we are able to represent natural numbers in a type-safe way! If a value is of type `Nat`, you know it cannot be negative, which is sometimes a nice guarantee to have [as aforementioned](#a-missing-puzzle-piece). Also, this is very similar to the [Peano axioms](https://en.wikipedia.org/wiki/Peano_axioms), which gives us very nice mathematical properties.\n\nHowever, this does not come without sacrificing some practicality: there is, as of writing this, no way to make the numeric literals have the type `Nat` instead of the built-in `int`. We still enjoy operators such as `+` or `*` thanks to their [corresponding magic methods](https://docs.python.org/3/reference/datamodel.html#emulating-numeric-types), but we will have to use functions to convert literals to our natural number type.\n\n## But why stop here?\n\n...We don't!\n\nWith the `type` statement added in Python 3.12 and structural pattern matching with `match`/`case` in 3.10, the language unlocked a lot of power at the type level. The latter, especially, is the best friend of inductive types ; and `Nat` is not the only one that is very useful!\n\nEspecially, I'm looking forward adding linked lists, inductive sets, trees, other numeric types that fit very well this little world.\n\n>[!IMPORTANT]\n> For now, only `Nat` is implemented, but it's just a matter of time before the others get added too \ud83d\ude04\n\n`inductive` also provides a submodule `builtins` which goal is to override existing built-ins to use better suited types: for example, `len` is replaced by `length`, which returns a `Nat`, more appropriated since `len` can never return a negative number.\n\n## Where does this idea come from?\n\nMore specifically, this library is heavily inspired by the proof assistant [Rocq](https://en.wikipedia.org/wiki/Coq_(software)) (previously known as Coq) and its programming language Gallina, which are based on a type theory called [calculus of constructions](https://en.wikipedia.org/wiki/Calculus_of_constructions), and more recently on its variant called [PCUIC](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.29) (predicative calculus of cumulative inductive constructions).\n",
"bugtrack_url": null,
"license": "MIT License Copyright (c) 2024 Qexat Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the \"Software\"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. THE SOFTWARE IS PROVIDED \"AS IS\", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. ",
"summary": "Inductive data structures for Python",
"version": "0.0.1.post1",
"project_urls": {
"source": "https://github.com/qexat/inductive"
},
"split_keywords": [
"inductive",
" data structures",
" nat",
" natural numbers",
" list",
" linked list",
" dependent typing"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "5ff51dbb637acfdb3736cd12af3127783c4baa6846d77c22c285a1fd50006f6f",
"md5": "e9c4d44756d7a1043092e3b546aaf527",
"sha256": "1d38604e910295d54bbd832c5e0bcc7c06a880052fd6f724dc2fdf90cab0a906"
},
"downloads": -1,
"filename": "inductive-0.0.1.post1-py3-none-any.whl",
"has_sig": false,
"md5_digest": "e9c4d44756d7a1043092e3b546aaf527",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.12",
"size": 9298,
"upload_time": "2024-12-06T07:46:23",
"upload_time_iso_8601": "2024-12-06T07:46:23.678580Z",
"url": "https://files.pythonhosted.org/packages/5f/f5/1dbb637acfdb3736cd12af3127783c4baa6846d77c22c285a1fd50006f6f/inductive-0.0.1.post1-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "6c3591163c832e010772064dd6c9d67952f2e185e1aec895e5512dbf33cca865",
"md5": "71370e3fc51131922eb4655e67f464d6",
"sha256": "fff7522d6be2f747a48b1713f60a157bf52916e715e91839f693941f7c8acb2a"
},
"downloads": -1,
"filename": "inductive-0.0.1.post1.tar.gz",
"has_sig": false,
"md5_digest": "71370e3fc51131922eb4655e67f464d6",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.12",
"size": 59358,
"upload_time": "2024-12-06T07:46:24",
"upload_time_iso_8601": "2024-12-06T07:46:24.916230Z",
"url": "https://files.pythonhosted.org/packages/6c/35/91163c832e010772064dd6c9d67952f2e185e1aec895e5512dbf33cca865/inductive-0.0.1.post1.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-12-06 07:46:24",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "qexat",
"github_project": "inductive",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"lcname": "inductive"
}