[Haskell-cafe] Restrictions on associated types for classes

[Dan Weston]

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.
> 
> Dan
> 
> Martin Sulzmann wrote:
>> 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 <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 ...
>>     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 <mailto:Haskell-Cafe at haskell.org>
>>     http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>