Type-checking for uniqueness in Dhall-Lang

#1

Hello, I am wondering if there is a way to type-check for uniqueness within Dhall, and how would it be recommended to be done.

For example, given a list of IP addresses, how would I check that the list contains no duplicates.

Extending on this, if given a list of records containing IP addresses, how could I efficiently check that these IP addresses are unique?

Can the type system be used for this?

Thanks.

1 Like
#2

There currently is no way to do this. See: https://github.com/dhall-lang/dhall-lang/issues/88

1 Like
#3

Hi Gabriel, thanks for your reply. I saw that, but I suppose I should change my question.

It has been years since I studied the theory.

Question: can a type-checking system even check for uniqueness without throwing a runtime error?

#4

If you can define an equality function for your IP address type, you can write a function duplicates : List IpAddress -> List IpAddress and check that a given list of addresses is unique with assert : duplicates myList === Prelude.List.empty IpAddress.

I believe Gabriel had documented a pattern for such tests somewhere, but I can’t find it right now.

#5

You might be thinking of: Config Validations

1 Like
#6

Thank you for the replies.

#7

I suppose it matters less with Dhall! Since config-generation time is approximately “compile time” one could in theory have a pass after typechecking.