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 <[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 ... > 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 > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe >
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
