[email protected]
[Top] [All Lists]

Re: [Haskell-cafe] Restrictions on associated types for classes

Subject: Re: [Haskell-cafe] Restrictions on associated types for classes
From: Jacques Carette
Date: Thu, 17 Dec 2009 10:58:17 -0500
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: [email protected] 
[mailto:[email protected]] 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
| [email protected]
| http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
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

<Prev in Thread] Current Thread [Next in Thread>