[mercury-users] dependent types with mercury

[Vladimir Gubarkov]

Thanks Chris for your explanation. This way it works indeed!

Though, error reported is rather criptic :-)
But, however, it is possible to distinguish odd & even size lists at compile
time. That's very interesting!


On Thu, Apr 7, 2011 at 7:06 PM, Chris King <colanderman at gmail.com> wrote:

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

I wish it could process in-depth )
Maybe mercury authors could make it more obvious in future releases...


>
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mercurylang.org/archives/users/attachments/20110407/786d0c12/attachment.html>