[Language] Contrib Organisation - idris-lang/Idris2 GitHub Wiki

General comments/discussion

@ohad: Some of the points become a bit less important if we also decide on an official package manager that supports meta-packages. For example, we can have a JSON, XML, SExpression parsing libraries, all in separate repos + packages, and a meta-package that installs them all.

@stefan-hoeck: Since #2584, Idris supports transitive package dependency resolution. This makes writing meta packages trivial: Just define an .ipkg file and list the packages you'd like to bundle under depends. By depending on the meta package, you'll transitively depend on the bundled packages. Pack, for instance, would therefore support meta packages out of the box.

So long as they have a consistent module hierarchy (like Text.JSON and Text.XML, and so on) the decision about where to stick everything is less important!

Existing package managers

Some package managers require specific backends to run (eg, inigo only runs where the nodeJS backend is available, I started a discussion there).

@ohad: I included some immediate dimensions for comparison off the top of my head, please add additional relevant ones!

Package	Source language	Dependencies	Packages from Git	scheme	racket	refC	nodeJS	maturity	notes
pack	Idris2	idris2, idris2api,toml,filepath	✓	✓	?	?	?	✓	uses a curated package collection
inigo	Idris2	idris2, idris2api,idrall	?	✘	✘	✘	✓	✓
elba	Rust	N/A	?	✘	✘	✘	✘	N/A	Only supports idris1 projects, needs porting
idris2-pkgs	Nix	nix-2-?	?	-	-	-	-	✓
sirdi	Idris2	collie	✓	✓	✓	✓	✓	✘	Still rough around the edges, unknown ETA to support basic functionality

Detailed analysis of `contrib`

Control/
- Algebra/ & Algebra.idr
  - Ellis: Need a separate algebra library.
- ANSI/ & ANSI.idr
  - Ellis: Seprate library for printing to ANSI terminal
- Arrow.idr & Category.idr
  - Ellis: Seprate library for category theory.
- Delayed.idr
  - Ellis: Not sure, simple enough that a user could just use an if in the type instead. But equally, could be put in base.
- Validation.idr
  - Ellis: Separate lib
- Linear
  - Ellis: Probably a separate library.
- Monad
  - Ellis: With "Control.Algebra".
Data/
- Binary/ & Binary.idr
  - Ellis: Even though its small, I think this should probably be moved to a separate library. I can see an argument for keeping it in base though, but persoanlly I don't think it's that universally useful.
- Container.idr
  - Ellis: Should be moved externally, maybe to a category theory library.
- Fin/
  - Ellis: Some individual functions might be worth moving to base, otherwise a lot of it is too niche and needs to be moved externally.
- Fun/
  - Ellis: I think this should be moved to an "n-ary functions" library or something.
- ~~HVect.idr~~ (Moved into base)
  - Ellis: This can be moved to base.
  - Gallais: It is superseded by All so should probably be deprecated
  - Matt: Agree about deprecating, though List.Quantifiers.All has an HList alias and that might be a good addition to Vect.Quantifiers.All just because of the name familiarity. There are a few utility functions that I think are worth porting regardless before moving to delete HVect from contrib.
  - NOTE: This has been partially moved on; there is an alias for HVect in base's Data.Vect.Quantifiers.All but there are likely still some nice utility functions to move from Data.HVect over to Data.Vect.Quantifiers before deleting Data.HVect from contrib entirely.
  - NOTE: https://github.com/idris-lang/Idris2/pull/3191
- IMaybe.idr
  - Ellis: Close, but I think this is not common enough to be in base.
  - Gallais: It is used in the compiler so should probably go in base.
  - Matt: I wonder if we need a stronger motivator than being used by the compiler (which I don't doubt IMaybe has). Text.Parser is also used by the compiler (not exactly the contrib one, but a pretty identical version) but I feel pretty good about that getting split off into it's own library.
- InductionRecursion/
  - Ellis: Not general enough, needs to be a separate library.
- Int/
  - Order.idr
    - Ellis: Not sure about this, need secondary input.
    - Matt: I'm open to being outvoted or outranked, but my gut here is to move this into a separate library. On one hand, it conceptually fits nicely with Nat.Order and Fin.Order but on the other hand I'd wager it is much less commonly used.
- Late.idr
  - Ellis: This is concise enough to be in base, but I'm not sure its commonly used enough to warrant it. Need others input.
  - Matt: Feels like a batteries included addition rather than a more minimalist take; I lean toward not moving this to base.
- Linear/
  - Array.idr
    - Ellis: Ideal candidate for a standalone library.
- List/
  - Algebra.idr
    - Ellis: Whatever happens with "Control.Algebra", this should go with it.
  - Alternating.idr
    - Ellis: Should be in an external library.
  - AtIndex.idr
    - Ellis: I think this is general enough to be moved into base.
  - Elem/
    - Ellis: I think some of these functions are useful enough to arguably fit into base. But I'm not sure on this one.
    - Matt: Agreed. It's not much to add and I always lean toward having proofs in base as long as they aren't too esoteric. Definitely a personal preference of mine, though.
  - Equalities.idr
    - Ellis: Some of these functions can maybe be moved to base.
  - Extra.idr
    - Ellis: I think this should be a separate library (too niche, or too easily composable from existing base functions).
  - ~~HasLength.idr~~ (Moved into base)
    - Ellis: I think this is general enough to be moved into base.
    - NOTE: https://github.com/idris-lang/Idris2/pull/2844
  - Lazy/ & Lazy.idr
    - Ellis: I think this should be a separate library.
  - Palindrome.idr
    - Ellis: Too niche, needs to be a separate library.
  - Reverse.idr
    - Ellis: I think this should be a separate library.
  - TailRec.idr
    - Ellis: Needs to be a separate library. Ideally this is made redundant with better compiler optimisations anyway.
  - Views/
    - Ellis: Should be moved to a separate library.
- Logic
  - Ellis: Ideally we just have a separate library for logic.
- Monoid
  - Ellis: Think this is too niche, needs to be separate.
- Morphisms
  - Ellis: Put this with "Control.Algebra"
- Nat
  - Ellis: Maybe just have a nat arithmetic library? I think the ackerman function should probably be ported from this and added as an example somewhere though.
- OpenUnion.idr
  - Ellis: Separate lib
- Oreder.idr
  - Ellis: Separate lib
- Path.idr
  - Ellis: Existing "Relation" part of base lib could be extended with this definition of reflexive transitive closure?
- Recursion
  - Ellis: Should be in a separate library.
- Rel
  - Ellis: I think this could be moved to base.
- SortedMap
  - Ellis: Separate lib
  - Matt: I think I would vote we promote this and the SortedSet to base. One argument could be along the lines raised above that they are useful enough to see use in the compiler. I think I've heard that folks would ideally like to see a shared interface for maps rather than settling on this one implementation, but I would personally rather take this because it's useful and somewhat proven and we have it right now and accept the possibility that at some point in the future we want to discuss a breaking change or removal in favor of something else.
  - Andre: I agree with Matt here, SortedMap is the closest thing we have to a Dictionary type which is a primitive expected to be available in most programming languages by default, so it should be in base. We have a slight issue about exporting a common interface between the dependent and the non-dependent version though. I would be infavor of including just the dependent version of SortedMap and introduce a non-dependent interface for other types of dictionaries (Hashmaps/non-dependent sorted map).
  - Falsifian: As an anecdote, a 5500-line Idris2 project of mine used nothing from contrib except SortedMap and SortedSet. I'm just an occasional Idris2 user, but to me it seems pretty important in a programming language to have a dictionary datatype available.
- SortedSet
  - Ellis: Separate lib
- Stream
  - Ellis: This function could be moved to base.
- String
  - Ellis: Parsers should definitely be a separate library in my opinion.
  - Matt: Agreed.
- Telescope
  - Ellis: Separate lib
- Tree
  - Ellis: Nice example but separate lib
- Validated.idr
  - Ellis: Separate lib
- Vect
  - Ellis: Some of this shuld definitely be separate, but need to go through every function as some may be suitable for base.
- Void
  - Ellis: Perhaps these should be moved to base?
  - Matt: Maybe? absurdity is just absurd with explicit zero-quantity. contradiction seems a little more useful. I suppose I'd use it if I ever remembered to.
Debug/
- Buffer.idr
  - Ellis: I think either this should be moved to base, or a separate "buffer" library should be made containing this and "Data.Buffer".
Decidable/
- Order/
  - Ellis: I'm not 100% on this one, but it sounds like it should be merged into the existing Relation stuff in base.
- Decidable/ & Finite/
  - Ellis: Need some secondary input on this one, not sure whether this is suitable for base.
Language/
- JSON/
  - Ellis: I think this should be moved to a specific JSON library.
Search/
- Ellis: I think this should be an external library.
Syntax/
- WithProof.idr
  - Ellis: Idris2 now supports the with..proof construct, this is redundant.
  - @ohad: Maybe the name is now misleading, but I have used this in the past, for example, inside a case statement where I also needed this proof (refactoring into a top-level declaration + with is not great. Maybe a principled solution is to add to our case statement a proof keyword, eg:
```
case foobar 3 proof prf of
  Blah => code requiring proof that foobar 3 === Blah
  Blar => code requiring proof that foobar 3 === Blar
```
  - Gallais: we should first make sure that the with..proof is not buggy e.g. that we don't suffer from https://github.com/agda/agda/issues/5668
- PreorderReasoning/
  - Ellis: Equational reasoning seems general enough to move to base. Not sure where exactly it should be moved to though.
  - @ohad: I think the plan is to have language support for equational reasoning that would make this defunct. In other libraries (eg Frex) I've used similar code for, say, setoids. That will probably become a part of an independent Setoid library.
System/
- Random.idr
  - Ellis: I'm actually not sure about this, I think it's small enough to be moved to base, but I could be swayed either way.
  - Matt: I could go either way too since I use Random infrequently enough to be on the fence but when I do use it I find it a pretty intuitive thing to live alongside file IO and access to system time and whatnot (so I vote move to base).
- Path.idr
  - Ellis: In it's current state, I don't like the idea of this being in base since it relies on the parsing library. Perhaps it would be better if the file APIs dealt with a "FilePath" data type rather than raw strings in the first place, potentially alleviating the need for this in the first place?
- Directory/
  - Ellis: Similar to Path.idr. Perhaps the most sensible short term solution is to bundle these together into an external library.
- Future.idr
  - Ellis: I think this should be moved to base.
  - Matt: Tough call because this is really just the first high level concurrent currency to be introduced so it's unfortunate to bless it just for that reason; then again, the test framework depends on it, so moving it out of this project seems like a bit of a drastic idea.
Text/
- Ellis: Most of this could just be refactored into a standalone parsing library.
- PrettyPrint/
  - Ellis: I think this should also be a standalone library.
- Distance/
  - Ellis: I think this should be a standalone library. It's only small, so there's an argument for bundling it with other things.