[m-dev.] Existentially quantified data constructors

[Ralph Becket]

Mark Brown, Tuesday, 15 April 2008:
> 
> Because they are not existentially quantified, and the constraint is
> introduced with '=>'.
> 
> All constraints have to be either universal (<=), meaning that all type vars
> occurring in it are universally quantified, or existential (=>), meaning that
> they are all existentially quantified.  You can't have half-half.
> 
> If you could, it wouldn't work very well with our implementation: universal
> constraints correspond to a typeclass_info with mode `in' (the caller proves
> that the constraint is satisfied) and existential constraints the mode is
> `out' (the callee proves it).  For a half-half constraint it wouldn't be so
> simple.  Where would the typeclass_info go?

Rats.

> Also, I suspect it wouldn't do what you think it might in the above case.

Really?  Rats, again.

The situation I have is the hybrid FD/LP solver instance needs to track
three things: the FD solver instance; the LP solver instance; the list
of LP/FD variable pairs for channelling bounds information.  The
variable types are functionally defined by the solver instance types.

I would like to write something like this:

:- type fdlp_solver(FDSolver, FDVar, LPSolver, LPVar)
	--->	fdlp_solver(
			FDSolver,
			LPSolver,
			list({LPVar, FDVar})
		).

:- type fdlp_var(FDVar, LPVar)
	--->	fdvar(FDVar)
	;	lpvar(LPVar).

:- instance flatzinc_solver(
		fdlp_solver(FDSolver, FDVar, LPSolver, LPVar),
		fdlp_var(FDVar, LPVar)
	)
	<=	(	flatzinc_solver(FDSolver, FDVar),
			flatzinc_solver(LPSolver, LPVar)
		)
	where [...].

But I can't because FDVar and LPVar appear more than once in the
instance declaration.  This means I have to hide the FDVar and LPVar
components of the fdlp_solver type:

:- type fdlp_solver(FDSolver, LPSolver)
	--->	fdlp_solver(
			FDSolver,
			LPSolver,
			list({univ, univ})
		).

Is there a better way than using univs here, given that I can't use
existential typing either?

-- Ralph
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------