[Haskell-cafe] Type Inference for Overloading without Restrictions

[Carlos Camarao]

On Wed, Jan 13, 2010 at 7:57 AM, Peter Verswyvelen <bugfact at gmail.com>wrote:

> A while ago, someone provided me a link to the paper "Type Inference
> for Overloading without Restrictions"
> http://www.dcc.ufmg.br/~camarao/ct-flops99.ps.gz<http://www.dcc.ufmg.br/%7Ecamarao/ct-flops99.ps.gz>
>
> Although I don't understand everything in this paper, I wander what
> people's opinions are about this regarding a future Haskell language
> revision or extension?
>

System CT (as it was defined in the Flops99 paper) is a core system
for constrained (parametric + ad-hoc) polymorphism, the main
difference with respect to Haskell type classes being that it uses a
closed world approach to overloading (as it was defined in the Flops99
paper),
while Haskell type classes uses an open world.

Open means that principal types of overloaded symbols are explicitly
specified (in Haskell class declarations), and, informally speaking,
satisfiability checking is performed only when overloading is resolved
(i.e. satisfiability is delayed until it cannot be delayed any longer).

Closed, on the other hand, means that principal types are determined
(inferred) according to (definitions available in) the context (as
occurs in the normal case, of non-overloaded symbols).

For details, see e.g. [1].

A "mixed" approach, where annotation of types of overloaded symbols is
not mandatory but satisfiability checking is done as in an open world
approach, is possible and advantageous.

Only prototype implementations exist to this date of system CT.
A prototype implementation of a mixed approach is currently under way.


>
> Would a feature like this be preferable over typeclasses?


The main disadvantage of system CT's closed world approach is the cost
of satisfiability checking. (However, this does not hold in the case of a
mixed
approach, where satisfiability checking is restrictd as in an open world).
The main advantage is that annotations (type classes) need not be mandatory
and a priori determined by the programmer.

Would it be practical to implement?


Yes, I think so, in particular the mixed approach where satisfiability
checking is
delayed (it is done only if there exist "unreachable variables" in the
constraint set),
as explained in [2].  We have recently sent a message with a link to our
paper, that
describes this approach, as a proposal to solve Haskell's MPTC dilemma
(without
the need of functional dependencies or another mechanism).


> Are people working on this?
>

Yes. We are.


> Thanks,
> Peter Verswyvelen
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>

Cheers,

Carlos

[1] Open and Closed World Approaches to Overloading: a Definition and
Support for
    Coexistence, Carlos Camarão, Cristiano Vasconcellos, Lucília Figueiredo,
João Nicola,
    Journal of Universal Computer Science 13(6), 854-873, 2007.
    http://www.dcc.ufmg.br/~camarao/CT/open-closed.pdf

[2] A Solution to Haskell's Multi-paramemeter Type Class Dilemma,
    Carlos Camarão, Rodrigo Ribeiro, Lucília Figueiredo, Cristiano
Vasconcellos,
    SBLP'2009 (13th Brazilian Symposium on Programming Languages), 2009.
    http://www.dcc.ufmg.br/~camarao/CT/solution-to-mptc-dilemma.pdf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100117/ee7f4f47/attachment.html