[m-users.] Referential integrity constraints in Mercury

[Dirk Ziegemeyer]

Hi Zoltan,

> Am 17.12.2020 um 08:50 schrieb Zoltan Somogyi <zoltan.somogyi at runbox.com>:
> 
> 
> 2020-12-17 07:09 GMT+11:00 "Dirk Ziegemeyer" <dirk at ziegemeyer.de>:
>> 
>> My questions are:
>> 1. Do you think it is possible to implement justified maps in Mercury at all?
>> 2. Do you think an idiomatic Mercury implementation could use existential types in order to make type signatures simpler than in [1]?
> 
> This is based on looking at the link you provided only for 15 or 20 minutes,
> so take this with a grain of salt, but I think the answer to both your questions is "no".

Thank you for your opinion. So I don’t need to follow this path further. Also because you opened my eyes for another solution …

> While Mercury implements the existential types that the Haskell version says it is missing,
> Mercury lacks support for rank 2 polymorphism, which seems even more essential
> for the functionality you are after. (By the way, *why* does it say that Haskell lacks existential types?
> We copied the idea from Haskell itself, a couple of decades ago.)
> 
>>   % A map associated with a phantom type P. P allows to attach evidence
>>   % to a key at type level that it exists in this map.
>>   %
>> :- type map(P, K, V)
>>   --->    map(map(K, V)).
> 
> Using the same name for three separate concepts is guaranteed to make
> any error messages harder to read than necessary :-(
> 
>>   % Convert a map into a justified map by adding type parameter P.
>>   %
>> :- some [P] func to_map(map(K, V)) = map(P, K, V).
> 
> I have no idea how you intend to make this work semantically. In the Haskell
> original, the phantom type parameter is alive *only* during a single function call,
> but here you are returning it for general use, with no restriction on the scope of P. 
> 
> As far as I can see, the compiler error you get for this (the first) works as intended.
> 
> The code of search_key is also missing the prefix that is required when you
> construct a new term of an existentially qualified type. (See section 11.3 of
> the language reference manual.) This is the proximate cause of the second
> error message.
> 
> While I applaud the intention behind the original Haskell work, it seems to me
> to have a very unfavourable effort to benefit ratio. The only ways to create what they call
> a key-with-evidence (evidence of being a key in a map) are to do a successful search
> in that map, and to enumerate all the keys in that map. In both cases, I would much prefer
> to simply record the value associated with each key in a tuple. Yes, it would cost
> some performance, but in Mercury, the impact would still be much smaller than
> the cost of laziness that Haskell users accept as a matter of course.
> 
> Zoltan.

Recording the value associated with each key sounds like a good solution. It should also be faster than searching the value associated with each key by calling map.search.

I have to remind myself that a Mercury application is not a relational database system where the speed-benefit of de-normalisation comes with the penalty of increased table size because copying data into a table is done by value and not by reference.

Dirk.