[email protected]
[Top] [All Lists]

Re: [Haskell-cafe] Restrictions on associated types for classes

Subject: Re: [Haskell-cafe] Restrictions on associated types for classes
From: Dan Weston
Date: Thu, 17 Dec 2009 13:08:28 -0800
Oops, reverse that. The *instance* declaration allows for infinite types, the *class* declaration does not.
Dan Weston wrote:
I think the denotational meanings are different. The instance also implies:

For each Cl t there must exist a Cl u where u does not unify with [v] for some v.
In other words, there must be a ground instance.

For the class declaration, the existence of a ground instance can be inferred only by excluding infinite types with strict type unification semantics. If infinite types were admitted (where type unification is done non-strictly), the class declaration allows for infinite types (let t ~ [t] in t). The instance does not.

Martin Sulzmann wrote:
The statements

class Cl [a] => Cl a


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).


[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
On Thu, Dec 17, 2009 at 6:40 PM, Simon Peyton-Jones
<[email protected] <mailto:[email protected]>> 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 ...
     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.

    Haskell-Cafe mailing list
    [email protected] <mailto:[email protected]>

Haskell-Cafe mailing list
[email protected]

<Prev in Thread] Current Thread [Next in Thread>