[mercury-users] dependent types with mercury

[Chris King]

Hi Vladmir, glad to see my post is generating some conversation!

On Thu, Apr 7, 2011 at 10:10 AM, Vladimir Gubarkov <xonixx at gmail.com> wrote:
> And thought, I could try to implement smth like even- (odd-) sized list
> using appropriate modes.

You can indeed do this.  The only "gotcha" is that the ---> shorthand
for inst definitions isn't as clever as you'd like.  What you wrote:

> :- inst even_list ---> [] ; [ground,ground|even_list]. % YYY

expands to this:

:- inst even_list ---> [] ; [ground | [ground|even_list]].

The ---> shorthand only works for the top-level constructors; so
Mercury thinks that the inner list cons is an inst rather than a
constructor.  To fix this you can write instead:

:- inst even_list ---> []; [ground | bound([ground | even_list])].

Then your code will compile as expected.  I've tested with a couple
functions that consume pairs of elements and it seems to work, but let
me know if you have any trouble.

Best,
Chris
--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------