[mercury-users] inst syntax? [was: Types as sets?]

[Ralph Becket]

Douglas Auclair, Wednesday, 12 February 2003:
> 
> Wow!  What an eye-opening way to create a limited type over a preexisting 
> type (er, sort of)!  In reviewing the Mercury language reference manual, I 
> saw no such way to create insts (although the Mercury library reference 
> does use that syntax), could a description of using ---> with insts be 
> added to the manual?

Working on it.

> Also I saw ---> and == for types, but the Mercury library contains types, 
> and insts, defined with = as well as ==.

In these cases, `=' is a synonym for `=='.

Personally I would rather we use `=' than `=='.  The (IMHO weak)
justification for using `==' in type, mode and inst declarations is that 
doing so obviates the need to put parentheses around func terms on the
RHS.  Personally, I'd rather we had just one symbol for equality, and
that that symbol be `='.

The inst definition

:- inst foo ---> bar ; baz ; quux.

is equivalent to writing

:- inst foo == bound(bar ; baz ; quux).

There's definitely scope for revisiting our syntax for inst definitions.

> I gather that ---> for inst 
> signifies a discriminated union for insts.  What is the purpose of = (vice 
> ==) for types and insts?  I guess in your example code above that 1; 2; 3; 
> ... are like mode states (like free or ground or unique), is that correct?  

No, 1, 2 and 3 are insts (instantiation states) meaning in this case
"bound to the functor 1", "bound to the functor 2" and "bound to the
functor 3".

> On a related topic, can an inst be built that is infinite in size (okay, 
> not "infinite", but how about "so large that it's impracticable to 
> enumerate the elements")?  How does one go about doing that?

:- inst list(I) ---> [] ; [I | list(I)].

describes an infinite set of insts.

> For example, the primitive type int has a large number of elements, and I 
> wish to construct the positive integers as a type (or inst) from int.  
> Also, I don't wish to use the Peano series to do it.  When I need 55, I'd 
> prefer to type 55 in the code, not s(s(... s(zero) ...)).  Is there a way 
> to create a type or inst that does this?

Not as such.

The general solution is to define an inst enumerating the subset of
interest of the supertype's insts.  To do so practically with int would
not be feasible in general, though, since int has such a large number of
data constructors.

> Or, generally, are there ways to 
> create types (or insts from pre-existing types) where enumeration is 
> impracticable, but all the elements are known (e.g. from a first element, a 
> successor/transformer function, and a termination test)?

Mark Brown's proposal handles this well for recursively defined types.

For instance, one could write

:- type list(T) ---> [] ; [T | list(T)].

:- subtype even_list(T) < list(T) ---> [] ; [T | odd_list(T) ].

:- subtype odd_list(T)  < list(T) --->      [T | even_list(T)].

Under Mark's proposal, subtyping like this is really a more convenient
way of defining and using complex insts.

> Where can I learn more about insts?  It is a concept that I have only read 
> about before, but that's it.  Are there papers/tutorials on insts 
> available, or some code (besides list.m and std_util.m) that uses insts 
> extensively?

There's actually not that much to an inst.  The section on "Insts, modes
and mode definitions" in the reference manual is pretty clear.

> By the way, writing a cryptarithmetic solver in straight Mercury was so 
> easy, thanks to the modes (and insts) of lists.  Not many programming 
> languages allow one to pass around a list of free variables so easily!

Er, the Mercury compiler doesn't (and maybe won't) handle partially
instantiated structures such as lists of unbound variables.  I think
your program may be working in a different way to that which you expect.

	Ralph
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------