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