[m-users.] Referential integrity constraints in Mercury

[Dirk Ziegemeyer]

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]?
 
Dirk

[1] https://hackage.haskell.org/package/justified-containers


%-----------------------------------------------------------------------------%
:- module justified_map.
%-----------------------------------------------------------------------------%

:- interface.

:- import_module map.


    % 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)).


    % A key that is guaranteed to exist in a map of type map(P, K, V)
    %
:- type key(P, K)
    --->    key(K).


    % Convert a map into a justified map by adding type parameter P.
    %
:- some [P] func to_map(map(K, V)) = map(P, K, V).


    % Search a key in a map.
    % Returns key that is guaranteed to exist in the map.
    % Fail if the map does not contain that key.
    %
:- pred search_key(map(P, K, _)::in, K::in, key(P, K)::out) is semidet.

%-----------------------------------------------------------------------------%

:- implementation.


to_map(X) = map(X).


search_key(map(Map), Key, key(Key)) :-
    map.contains(Map, Key).

%-----------------------------------------------------------------------------%

:- module test_justified_map.
%-----------------------------------------------------------------------------%

:- interface.

:- import_module io.


:- pred main(io::di, io::uo) is det.

%-----------------------------------------------------------------------------%

:- implementation.

:- import_module justified_map.

:- import_module list.
:- import_module map.
:- import_module pair.


main(!IO).


:- func get_test_map = map(P, int, string).

get_test_map =
    to_map(map.from_sorted_assoc_list([
        5 - "a",
        3 - "b"
    ])).

%-----------------------------------------------------------------------------%

Compiler errors:

justified_map.m:034: In function `to_map'/1:
justified_map.m:034:   warning: unresolved polymorphism.
justified_map.m:034:   The variable with an unbound type was:
justified_map.m:034:     HeadVar__2: justified_map.map(P, K, V)
justified_map.m:034:   The unbound type variable will be implicitly bound to
justified_map.m:034:   the builtin type `void'.
justified_map.m:034:   The body of the clause contains a call to a polymorphic
justified_map.m:034:   predicate, but I can't determine which version should be
justified_map.m:034:   called, because the type variables listed above didn't
justified_map.m:034:   get bound. (I ought to tell you which call caused the
justified_map.m:034:   problem, but I'm afraid you'll have to work it out
justified_map.m:034:   yourself. My apologies.)
Making Mercury/cs/test_justified_map.c
test_justified_map.m:038: In clause for function `get_test_map'/0:
test_justified_map.m:038:   in function result term of clause head:
test_justified_map.m:038:   type error in unification of variable `HeadVar__1'
test_justified_map.m:038:   and functor `to_map'/1.
test_justified_map.m:038:   variable `HeadVar__1' has type `(some [P]
test_justified_map.m:038:   justified_map.map(P, int, string))',
test_justified_map.m:038:   functor `to_map'/1 has type
test_justified_map.m:038:   `to_map(tree234.tree234(K, V)): (some [P]
test_justified_map.m:038:   justified_map.map(P, K, V))'.
test_justified_map.m:038:   The partial type assignment was:
test_justified_map.m:038:     some [P_1]
test_justified_map.m:038:     HeadVar__1_1: justified_map.map(P, int, string)