idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.46k stars 368 forks source link

[ contrib ] Add Data.UUID #3244

Closed glmxndr closed 1 month ago

glmxndr commented 3 months ago

Description

Adding a simple UUID implementation in contrib. I know that there is an effort to declutter contrib, and asked in the discord where it should go. It seemed to be ok to put it in base, but as it is generally more useful to have access to randomly generated UUIDs, this requires access to System.Random, which is in contrib.

There is a separate file, which is not listed in the contrib.ipkg and thus should not be exposed, dealing with hexadecimal representation of Bits8, Bits16, etc. This is something I have found missing in base / contrib, but as it is my first PR I wished to keep focused on one thing.

Should this change go in the CHANGELOG?

stefan-hoeck commented 3 months ago

I wonder, why this should not just go to a separate library. Alternatively, move System.Random to base, if it is required there, but adding new stuff to contrib will just create more work later on.

mattpolzin commented 3 months ago

I'd be amenable to moving System.Random into base. We were on the fence about that module when doing a full review of contrib, but I lean toward moving it into base myself. I'm not making that decision with this comment, just voting that direction.

buzden commented 3 months ago

As an author of an alternative library with somewhat similar but competing interfaces, I must be biased, but what I dislike about moving current implementation of System.Random to base is it's rigidity. It is very IO-oriented and putting it to base looks like saying "this is the way to do it". If it either was redesigned to be able to support both pure and IO-based approaches, or at least being renamed to state explicitly that it is IO-based would be good in my point of view.

gallais commented 3 months ago
  1. I think that by default any additions to contrib should be rejected as we want to get rid of the package altogether
  2. I agree with @buzden that an MTL-style interface like we already have for state & co would be preferable for Randomness
mattpolzin commented 3 months ago

Sounds like good reasons not to move the existing Random module into base to me.

I suppose we have a few paths that could be discussed.

  1. This UUID module would make a fine third party package and could be included in the wiki and pack's collection etc. if not even hosted under idris-community (author's choice).
  2. We could work towards a design of Random that is acceptable in base.
  3. The UUID module could defer randomness to an interface that allows the user to choose how to give it random numbers; perhaps that interface itself is a reasonable generalization of Random to be useful broadly in base?
mattpolzin commented 2 months ago

I think there's one last option too: support UUID handling other than random creation now and let random creation be the only bit that needs to be considered further. Although it's true that generating new UUIDs is incredibly useful, it is also useful to be able to handle existing UUIDs in its own right.

glmxndr commented 2 months ago

I suppose I could just change the randomUUID function to one that takes 2 Bit64 and returns a valid Version 4 UUID by setting the correct bits.

(I don't think I would provide a better proposal that @buzden 's ones for random interfaces anyways. But I feel it's out of scope for this PR.)