[m-users.] Referential integrity constraints in Mercury

[Zoltan Somogyi]

2020-12-17 07:09 GMT+11:00 "Dirk Ziegemeyer" <dirk at ziegemeyer.de>:
> Hi,
> relational databases have the concept of referential integrity which puts a constraint on a foreign key that it must exist as primary key in another table.
> 
> I’d love to get a compile-time guarantee from Mercury that a certain key exists in a map.
> 
> Example:
> - Collection with primary keys: map(int, string)
> - Collection with foreign keys: list(int)
> Mercury does not prevent me from using any int as foreign key, which might cause my application to abort at runtime when calling map.lookup.
> 
> There is a Haskell module Data.Map.Justified [1] which enforces referential integrity by attaching a phantom type variable P to the map and the key:
> :- type map(P, K, V) ---> map(K, V).
> :- type key(P, K) ---> key(K).
> 
> You can obtain a key(P, K) by checking if it is an actual member of map(P, K, V). The implementation in [1] guarantees that „… the proof that a key is present can't leak to contexts where the proof would no longer be valid.“
> 
> The type signatures in [1] look strange, because „The problem is that Haskell doesn't support existential types directly: the exists part of the type we wrote out is just wishful thinking. Instead, we have to go about things a little indirectly: we'll encode existentially-quantified types, via rank-2 universally-quantified types.“
> 
> I’d like to implement a module justified_map in Mercury. My first attempt (see below) is different from [1], because Mercury seems to support existentially typed predicates and functions. I did not use Mercury’s existential types before and ran into compiler errors with my first try.
> 
> 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".

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.