james
/
monoids-in-the-category-of-endofunctors
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
monoids-in-the-category-of-.../README.md

15 lines
677 B
Markdown
Raw Permalink Normal View History

Working on improving documentation.
2020-10-29 18:48:11 -07:00
# Monoids in the Category of Endofunctors
This is a **toy** library for studying the field of [Abstract Nonsense](https://en.wikipedia.org/wiki/Abstract_nonsense) through Haskell.
Rewrite. I ended up re-implementing most of the functionality of this library while trying to implement a categorical model of a programming language I was working on, so I went ahead and copied most of it over here. The new version is still missing some features, such as linear functions, monadic bind, the Unc typeclass, and haddock. It also makes a few different design decisions, which come with their own trade-offs.
2024-01-04 15:11:41 -08:00
Writing this sort of code makes for a fun puzzle,
but you probably shouldn't use this for any serious work.
Splitting off levels of generality by morality.
2020-10-20 20:07:38 -07:00
Working on improving documentation.
2020-10-29 18:48:11 -07:00
This library currently includes:
Rewrite. I ended up re-implementing most of the functionality of this library while trying to implement a categorical model of a programming language I was working on, so I went ahead and copied most of it over here. The new version is still missing some features, such as linear functions, monadic bind, the Unc typeclass, and haddock. It also makes a few different design decisions, which come with their own trade-offs.
2024-01-04 15:11:41 -08:00
* Category theory
* Recursion schemes (`Functor.Algebra`)
Working on improving documentation.
2020-10-29 18:48:11 -07:00
* Dependent types, type-level programming, and codata (`Data`)
Rewrite and generalize most of the library; partial LinearTypes support. I had to move back to explicit arguments rather than associated types as my representation of categories because a functor may be a functor in multiple categories (e.g. ((,) a) is a functor in both the category of linear and intuitionistic implication). This also allowed me to get rid of some bad boilerplate involving `(:~:)` and some related issues. I also finally managed to get Monads as monoids in the category of endofunctors again. I don't recall what prevented me from doing it in the last iteration, but I think it's probably working now. It could just be that I understand the theory better and it's easier for me to get right now. There's still some unimplemented stuff that I'd like, pretty bad usability issues that I'd like to work around, and a dire lack of documentation. I intend to work on all that soon. The stack stuff has been removed because stackage doesn't have GHC 9 yet, and the template-haskell stuff has been removed until I can rewrite it, seeing as it was essentially useless as it was. The LinearTypes support is very incomplete, but it's supported in some places and I don't think I'd have much trouble expanding to support it in general; I just haven't had much time to experiment with it yet.
2021-03-01 02:01:22 -08:00
* Dependent quantifiers (implemented with the help of a typeclass; `Quantifier`)
Splitting off levels of generality by morality.
2020-10-20 20:07:38 -07:00
Working on improving documentation.
2020-10-29 18:48:11 -07:00
## Content warning
This library is an abuse of GHC Haskell and an abuse of common sense.
Do not attempt to view this library if you are faint of heart.