Way to create user-accessible unique values

#1

Bit of a strange question, but I’m pondering what is the “best” way to allow a user to create an easily-accessible number of distinct values, e.g. that might serve as unique IDs. Note: I’m probably going to use Naturals throughout, but I don’t care what the values are, so long as they can be converted to unique Text.

Basically, at the end of the day, I need a user to be able to make a record or union type that maps to unique values, e.g. either:

let IDs = { key1 = 1
, key2 = 2
, key3 = 3
}

in  IDs.key2

or

let IDs = < Key1 | Key2 | Key3 >

let getVal : IDs -> Natural = merge ...

in getVal IDs.Key1

without having to write the = 1, = 2 or getVal by hand.

For example, the “perfect” case would be something like this (not possible in Dhall, I’m sure):

makeIDs ["key1", "key2", "key3"]

returning

{ key1 = 1
, key2 = 2
, key3 = 3
}

Since Maps are not accessible by their keys, this can’t be done nicely using them.

Is there any possible solution that at least ensures that a simple typo can’t create a non-unique value?

#2

You can get pretty close by generating an association list in this way:

let Prelude = https://prelude.dhall-lang.org/package.dhall

let makeIDs =
      λ(keys : List Text) →
        let adapt =
              λ(element : { index : Natural, value : Text }) →
                { mapKey = element.value, mapValue = element.index }

        in  Prelude.List.map
              { index : Natural, value : Text }
              { mapKey : Text, mapValue : Natural }
              adapt
              (Prelude.List.indexed Text keys)

let example =
        assert
      :   makeIDs [ "key1", "key2", "key3" ]
        ≡ [ { mapKey = "key1", mapValue = 0 }
          , { mapKey = "key2", mapValue = 1 }
          , { mapKey = "key3", mapValue = 2 }
          ]

in  makeIDs

The main thing you’d be missing is a fromMap utility, like the one proposed here:

#3

Yeah, getting to the Map was always nice and convenient, it’s just the lack of fromMap. I do think that something like that builtin would be a great addition to the language (unless it causes problems unforeseen by me), since there isn’t really any way to programmatically generate records at the moment in Dhall, when DRY is one of the big selling points of the language. Especially as Dhall itself continues to become more important as an actual consumed endpoint, rather than an intermediate step to JSON (where Maps do this already).