> So, we are allowed to use (..) at any place in the
> context (or maybe even type), to show the compiler
> that you know "something" should be there.
HAL has this feature. HAL ressembles Mercury, but with support for
constraint solvers and with real logical variables.
Syntax is ? instead of the .. and it is allowed anywhere in a
pred or mode declaration and even in the type class constraints on
predicates. The HAL compiler infers the question marks (currently only
implemented for types/classes) - it needs to because it compiles to
Mercury.
The approach is based on using constraint solving; if at the
end of the inference, there are no constraints on ?, that means it is
polymorphic. Maria Garcia de la Banda implemented this - and is
extending the compiler. Other people in the HAL project are Peter
Stuckey, Kim Marriott, Warwick Harvey and myself. Maria says it is not
a big implementation effort to have this ? - but I guess this depends
on what framework one started with.
At the K.U.Leuven, Marc De Necker has together with a student,
implemented a type inferencer using abduction with a similar feature
(although syntactically completely different); there, the .. (or ?) is
allowed even in the type definitions. Abduction in this case is close
to constraint solving (in spirit at least).
By the end of next week, there should be a home page for HAL at
http://www.csse.monash.edu.au/~mbanda/hal
Bart Demoen
