[Haskell-cafe] Restrictions on associated types for classes
westondan at imageworks.com
Thu Dec 17 15:57:51 EST 2009
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 .
> 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  (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).
>  Cordelia V. Hall, Kevin Hammond
> Simon L. Peyton Jones
> Philip Wadler
> Type Classes in Haskell. ACM Trans. Program. Lang. Syst. 18
> 109-138 (1996)
>  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
> <simonpj at microsoft.com <mailto: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 ...
> 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
> Haskell-Cafe at haskell.org <mailto:Haskell-Cafe at haskell.org>
More information about the Haskell-Cafe