[Haskell-cafe] Restrictions on associated types for classes

[Martin Sulzmann]

The statements

class Cl [a] => Cl a

and

instance Cl a => Cl [a]

(I omit the type family constructor in the head for simplicyt)

state the same (logical) property:

For each Cl t there must exist Cl [t].

Their operational meaning is different under the dictionary-passing
translation [1].
The instance declaration says we build dictionary Cl [a] given the
dictionary Cl [a]. The super class declaration says that the dictionary for
Cl [a]
must be derivable (extractable) from Cl a's dictionary. So, here
we run into a cycle (on the level of terms as well as type inference).

However, if we'd adopt a type-passing translation [2] (similar to
dynamic method lookup in oo languages) then there isn't
necessarily a cycle (for terms and type inference). Of course,
we still have to verify the 'cyclic' property which smells like
we run into non-termination if we assume some inductive reason
(but we might be fine applying co-induction).

-Martin

[1] Cordelia V. Hall, Kevin
Hammond<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/h/Hammond:Kevin.html>,
Simon L. Peyton
Jones<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/j/Jones:Simon_L=_Peyton.html>,
Philip Wadler<http://www.informatik.uni-trier.de/%7Eley/db/indices/a-tree/w/Wadler:Philip.html>:
Type Classes in Haskell. ACM Trans. Program. Lang. Syst.
18<http://www.informatik.uni-trier.de/%7Eley/db/journals/toplas/toplas18.html#HallHJW96>(2):
109-138 (1996)

[2] Satish R. Thatte: Semantics of Type Classes Revisited. LISP and
Functional Programming
1994<http://www.informatik.uni-trier.de/%7Eley/db/conf/lfp/lfp1994.html#Thatte94>:
208-219

On Thu, Dec 17, 2009 at 6:40 PM, Simon Peyton-Jones
<simonpj at microsoft.com>wrote:

> | > Hmm.  If you have
> | >   class (Diff (D f)) => Diff f where
> | >
> | > then if I have
> | >     f :: Diff f => ...
> | >     f = e
> | > then the constraints available for discharging constraints arising
> | > from e are
> | >     Diff f
> | >     Diff (D f)
> | >     Diff (D (D f))
> | >     Diff (D (D (D f)))
> | >     ...
> | >
> | > That's a lot of constraints.
> |
> | But isn't it a bit like having an instance
> |
> |    Diff f => Diff (D f)
>
> A little bit.  And indeed, could you not provide such instances?  That is,
> every time you write an equation for D, such as
>         type D (K a) = K Void
> make sure that Diff (K Void) also holds.
>
> The way you it, when you call f :: Diff f => <blah>, you are obliged to
> pass runtime evidence that (Diff f) holds.  And that runtime evidence
> includes as a sub-component runtime evidence that (Diff (D f)) holds.   If
> you like the, the evidence for Diff f looks like this:
>        data Diff f = MkDiff (Diff (D f)) (D f x -> x -> f x)
> So you are going to have to build an infinite data structure.  You can do
> that fine in Haskell, but type inference looks jolly hard.
>
> For example, suppose we are seeking evidence for
>        Diff (K ())
> We might get such evidence from either
>  a) using the instance decl
>         instance Diff (K a) where ...
> or
>  b) using the fact that (D I) ~ K (), we need Diff I, so
>        we could use the instance
>          instance Diff I
>
> Having two ways to get the evidence seems quite dodgy to me, even apart
> from the fact that I have no clue how to do type inference for it.
>
> Simon
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20091217/1663d52b/attachment-0001.html