[Haskell-cafe] Restrictions on associated types for classes

[Jacques Carette]

Which is 'right' in a way, since in the language Conor defined, all 
definable terms are "infinitely differentiable", and that can be 
inferred from the given rules.  That, in practice, you only need a 
finite number of them in any given computation is derivable from the 
instances, but is not a general theorem.

Jacques

PS: wait until someone wants to define resurgent functions, where you 
need ordinals to keep track of similar information!  Nice thing is that 
it's all still computable, you just have to work a fair bit harder to 
set up the correct machinery.  See papers by Salvy & Shackell, as well 
as van der Hoeven.

Simon Peyton-Jones 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.  
>
> Simon
>
>
> | -----Original Message-----
> | From: haskell-cafe-bounces at haskell.org [mailto:haskell-cafe-bounces at haskell.org] On
> | Behalf Of Conor McBride
> | Sent: 17 December 2009 14:48
> | To: Haskell Cafe
> | Subject: Re: [Haskell-cafe] Restrictions on associated types for classes
> | 
> | Hi all
> | 
> | On 17 Dec 2009, at 14:22, Tom Schrijvers wrote:
> | 
> | >> class MyClass k where
> | >> type AssociatedType k :: *
> | >>
> | >> Is there a way of requiring AssociatedType be of class Eq, say?
> | >
> | > Have you tried:
> | >
> | > {-# LANGUAGE TypeFamilies #-}
> | > {-# LANGUAGE FlexibleContexts #-}
> | >
> | > class Eq (AssociatedType k) => MyClass k where
> | >  type AssociatedType k :: *
> | 
> | I just got very excited about this. I'm supposed to be
> | setting a test, but this is far more interesting. I tried
> | this
> | 
> |  > {-# LANGUAGE TypeFamilies, FlexibleContexts, EmptyDataDecls,
> | TypeOperators #-}
> | 
> |  > module DDD where
> | 
> |  > class (Diff (D f)) => Diff f where
> |  >   type D f
> |  >   plug :: D f x -> x -> f x
> | 
> |  > newtype K a x = K a deriving Show
> | 
> |  > data Void
> |  > magic :: Void -> a
> |  > magic x = x `seq` error "haha"
> | 
> |  > instance Diff (K a) where
> |  >   type D (K a) = K Void
> |  >   plug (K c) x = magic c
> | 
> |  > newtype I x = I x deriving Show
> | 
> |  > instance Diff I where
> |  >   type D I = K ()
> |  >   plug (K ()) x = I x
> | 
> |  > data (f :+: g) x = L (f x) | R (g x) deriving Show
> | 
> |  > instance (Diff f, Diff g) => Diff (f :+: g) where
> |  >   type D (f :+: g) = D f :+: D g
> |  >   plug (L f') x = L (plug f' x)
> |  >   plug (R g') x = R (plug g' x)
> | 
> |  > data (f :*: g) x = f x :& g x deriving Show
> | 
> |  > instance (Diff f, Diff g) => Diff (f :*: g) where
> |  >   type D (f :*: g) = (D f :*: g) :+: (f :*: D g)
> |  >   plug (L (f' :& g)) x = plug f' x :& g
> |  >   plug (R (f :& g')) x = f :& plug g' x
> | 
> | But I got this message
> | 
> | [1 of 1] Compiling DDD              ( DDD.lhs, interpreted )
> | 
> | DDD.lhs:5:2:
> |      Cycle in class declarations (via superclasses):
> |        DDD.lhs:(5,2)-(7,28): class (Diff (D f)) => Diff f where {
> |                                  type family D f; }
> | Failed, modules loaded: none.
> | 
> | and now I have to go back to setting my class test.
> | 
> | Sorry for spam
> | 
> | Conor
> | 
> | _______________________________________________
> | Haskell-Cafe mailing list
> | Haskell-Cafe at haskell.org
> | http://www.haskell.org/mailman/listinfo/haskell-cafe
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>