Currently we have class Functor c where fmap :: (x -> y) -> (c x -> c y) This relies on c having kind * -> *. For example, Bytestring cannot be an instance of Functor. A cleaner solution would be to have something like class Container c where type Element c :: * I then attempted to write class Container c => Functor c where fmap :: (Functor cx, Functor cy, Element cx ~ x, Element cy ~ y) => (x -> y) -> (cx -> cy) However, this fails horribly: The type signature fails to mention c. And even if it did, this type signature still isn't correct: It says that fmap can transform *any* functor into *any* other functor, which is wrong. It seems that we have gained the ability to talk about containers holding any type of value (even hard-coded types or types with class constraints), but lost the ability to refer to a particular "type of" functor without also specifying the element type. Does anybody know a straightforward way to fix this? Or is this just a dead end?
Andrew Coppin
Currently we have
class Functor c where fmap :: (x -> y) -> (c x -> c y)
This relies on c having kind * -> *. For example, Bytestring cannot be an instance of Functor.
A cleaner solution would be to have something like
class Container c where type Element c :: *
Yes, and I already have ideas and plan to write a library containing such a class (not sure whether I'll stick to ATs or MPTCs+fundeps though).
I then attempted to write
class Container c => Functor c where fmap :: (Functor cx, Functor cy, Element cx ~ x, Element cy ~ y) => (x -> y) -> (cx -> cy)
However, this fails horribly: The type signature fails to mention c. And even if it did, this type signature still isn't correct: It says that fmap can transform *any* functor into *any* other functor, which is wrong.
ListLike does this, and I agree that it's a problem.
It seems that we have gained the ability to talk about containers holding any type of value (even hard-coded types or types with class constraints), but lost the ability to refer to a particular "type of" functor without also specifying the element type.
Does anybody know a straightforward way to fix this? Or is this just a dead end?
I've worked out a way around doing this in the current state of the experimental replacement for fgl: define a new class that tries to force the parametrism back into the non-parametric structure. However, since super-class constraints are currently not available the resulting type sigs are very, very ugly: ,---- | class (InductiveGraph (g n e)) => MappableGraph g n e where | | gmap :: (InductiveGraph (g n' e')) => (Context (g n e) -> Context (g n' e')) | -> g n e -> g n' e' | gmap f = fromContexts . map f . toContexts | | nmap :: ( InductiveGraph (g n' e) | , Node (g n e) ~ Node (g n' e) | , EdgeLabel (g n e) ~ EdgeLabel (g n' e)) | => (NodeLabel (g n e) -> NodeLabel (g n' e)) | -> g n e -> g n' e | nmap f = gmap f' | where | f' (Context ei n l eo) = Context ei n (f l) eo | | emap :: ( InductiveGraph (g n e') | , Node (g n e) ~ Node (g n e') | , NodeLabel (g n e) ~ NodeLabel (g n e')) | => (EdgeLabel (g n e) -> EdgeLabel (g n e')) | -> g n e -> g n e' | emap f = gmap f' | where | f' (Context ei n l eo) = Context (applyF ei) n l (applyF eo) | applyF = map (second f) `---- -- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com IvanMiljenovic.wordpress.com
Hello Andrew The non-type-changing map is sometimes useful as a type class - in my graphics lib Wumpus, I call it pointwise: class Pointwise sh where type Pt sh :: * pointwise :: (Pt sh -> Pt sh) -> sh -> sh For the graphics I want objects to be parametric on unit (which is usually Double), i.e.: data Point2 u = P2 !u !u But I usually don't want to deeply map on the unit, for instance a bounding box is represented as two corner points, bottom-left and top-right - for affine transformations I want to map on the points rather than the unit-of-points, so the Pointwise instance is: instance Pointwise (BoundingBox u) where type Pt (BoundingBox u) = Point2 u pointwise f (BBox bl tr) = BBox (f bl) (f tr) Where Bounding Box is: data BoundingBox u = BBox { ll_corner :: Point2 u , ur_corner :: Point2 u } I've seen this typeclass appear on the Cafe a couple of times under different names of course.
On Jul 3, 2010, at 4:39 PM, Andrew Coppin wrote:
class Container c => Functor c where fmap :: (Functor cx, Functor cy, Element cx ~ x, Element cy ~ y) => (x -> y) -> (cx -> cy)
However, this fails horribly: The type signature fails to mention c.
You have to mention c, this means an extra argument to fmap. But if you do that you also get the opportunity to restrict what x and y can be. As you'll have to pass around this extra argument, it will usually be easier to just pass around the map function though.
type family F f a :: * class RFunctor f where (%) :: f a b -> (a -> b) -> F f a -> F f b
Then you can make ByteString an instance using a GADT:
data BSFunctor :: * -> * -> * where BS :: BSFunctor Word8 Word8 type instance F BSFunctor Word8 = B.ByteString instance RFunctor BSFunctor where BS % f = B.map f
Regular functors are still instances as well of course.
data Ftor :: (* -> *) -> * -> * -> * where Ftor :: Functor f => Ftor f a b type instance F (Ftor f) a = f a instance RFunctor (Ftor f) where Ftor % f = fmap f
Set can be an instance too:
data SetFunctor :: * -> * -> * where SetF :: (Ord a, Ord b) => SetFunctor a b type instance F SetFunctor a = Set.Set a instance RFunctor SetFunctor where SetF % f = Set.map f
Or Strings. Let's do 3 functors in one take:
data StringFunctor :: * -> * -> * where EachChar :: StringFunctor Char Char EachWord :: StringFunctor String String EachLine :: StringFunctor String String type instance F StringFunctor a = String instance RFunctor StringFunctor where EachChar % f = map f EachWord % f = unwords . map f . words EachLine % f = unlines . map f . lines
And finally the identity functor and functor composition.
data Id a b = Id type instance F Id a = a instance RFunctor Id where Id % f = f
data (:.:) :: (* -> * -> *) -> (* -> * -> *) -> * -> * -> * where (:.:) :: (RFunctor g, RFunctor h) => g (F h a) (F h b) -> h a b -> (g :.: h) a b type instance F (g :.: h) a = F g (F h a) instance RFunctor (g :.: h) where (g :.: h) % f = g % (h % f)
Functor composition requires UndecidableInstances, because of the nested type family application. Perhaps one day GHC will be able to tell that this is structural recursion, and therefore not undecidable. This is a variation on what I'm doing in data-category 0.2, which is not done yet, but you can take a look here: http://github.com/sjoerdvisscher/data-category/ greetings, Sjoerd Visscher
Sjoerd Visscher wrote:
On Jul 3, 2010, at 4:39 PM, Andrew Coppin wrote:
class Container c => Functor c where fmap :: (Functor cx, Functor cy, Element cx ~ x, Element cy ~ y) => (x -> y) -> (cx -> cy)
However, this fails horribly: The type signature fails to mention c.
You have to mention c, this means an extra argument to fmap. But if you do that you also get the opportunity to restrict what x and y can be.
Well, you can say class Container cy => Functor cy where fmap :: (Functor cx, Element cx ~ x, Element cy ~ y) => (x -> y) -> (cx -> cy) But that's still wrong.
As you'll have to pass around this extra argument, it will usually be easier to just pass around the map function though.
type family F f a :: * class RFunctor f where (%) :: f a b -> (a -> b) -> F f a -> F f b
I have literally no idea what a type family is. I understand ATs (I think!), but TFs make no sense to me. (For this reason, most if not all of the rest of this post doesn't make sense.)
On Jul 4, 2010, at 11:31 AM, Andrew Coppin wrote:
type family F f a :: * class RFunctor f where (%) :: f a b -> (a -> b) -> F f a -> F f b
I have literally no idea what a type family is. I understand ATs (I think!), but TFs make no sense to me.
(For this reason, most if not all of the rest of this post doesn't make sense.)
I would have liked to use ATs here, like this:
class RFunctor f where type F f a :: * (%) :: f a b -> (a -> b) -> F f a -> F f b
But this isn't valid as ATs require all type variables to be in scope, and 'a' isn't. There's a GHC ticket for this: http://hackage.haskell.org/trac/ghc/ticket/3714 However, I think type families are actually easier to understand than ATs, you can see them as functions on types. So:
type family F f a :: *
This declares a "function" F with two arguments, f and a, which "returns" a type of kind *
type instance F BSFunctor Word8 = B.ByteString
This declares that F applied to BSFunctor and Word8 is the type ByteString. So if we take all this together:
data BSFunctor :: * -> * -> * where BS :: BSFunctor Word8 Word8 type instance F BSFunctor Word8 = B.ByteString instance RFunctor BSFunctor where BS % g = B.map g
It helps to write out what the type of BS % g needs to be. BS is of type BSFunctor Word8 Word8, so a and b both are Word8, and F BSFunctor a and F BSFunctor b are both B.ByteString. So the specialized type of (%) is:
BSFunctor Word8 Word8 -> (Word8 -> Word8) -> B.ByteString -> B.ByteString
I admit that 'F' and '%' aren't very enlightening names. As functors map both types and functions, the following may be more readable, with TMap mapping types, and fmap mapping functions:
type family TMap f a :: * class RFunctor f where fmap :: f a b -> (a -> b) -> f `TMap` a -> f `TMap` b
With as example the list functor:
data List a b = List type instance List `TMap` a = [a] instance RFunctor List where List `fmap` f = map f
I hope this helps. greetings, Sjoerd Visscher
On 07/04/2010 01:49 PM, Sjoerd Visscher wrote:
On Jul 4, 2010, at 11:31 AM, Andrew Coppin wrote:
type family F f a :: * class RFunctor f where (%) :: f a b -> (a -> b) -> F f a -> F f b
I have literally no idea what a type family is. I understand ATs (I think!), but TFs make no sense to me.
(For this reason, most if not all of the rest of this post doesn't make sense.)
I would have liked to use ATs here, like this:
class RFunctor f where type F f a :: * (%) :: f a b -> (a -> b) -> F f a -> F f b
But this isn't valid as ATs require all type variables to be in scope, and 'a' isn't. There's a GHC ticket for this: http://hackage.haskell.org/trac/ghc/ticket/3714
This works (on my ghc-6.12.2):
class Rfunctor f where type F f :: * -> * (%) :: f a b -> (a -> b) -> F f a -> F f b
[...]
-- Steffen
On Jul 4, 2010, at 1:58 PM, Steffen Schuldenzucker wrote:
This works (on my ghc-6.12.2):
class Rfunctor f where type F f :: * -> * (%) :: f a b -> (a -> b) -> F f a -> F f b
Yes, but then this isn't allowed: data BSFunctor :: * -> * -> * where BS :: BSFunctor Word8 Word8 instance RFunctor BSFunctor where type F BSFunctor Word8 = B.ByteString BS % f = B.map f -- Sjoerd Visscher
On Sun, Jul 04, 2010 at 10:31:34AM +0100, Andrew Coppin wrote:
I have literally no idea what a type family is. I understand ATs (I think!), but TFs make no sense to me.
ATs are just TFs which happen to be associated with a particular class. So if you understand ATs then you understand TFs too, you just didn't know it. =) -Brent
Brent Yorgey wrote:
On Sun, Jul 04, 2010 at 10:31:34AM +0100, Andrew Coppin wrote:
I have literally no idea what a type family is. I understand ATs (I think!), but TFs make no sense to me.
ATs are just TFs which happen to be associated with a particular class. So if you understand ATs then you understand TFs too, you just didn't know it. =)
How would that make sense though? I'm having trouble forming a mental image of how / why you'd use that...
Andrew Coppin wrote:
Brent Yorgey wrote:
On Sun, Jul 04, 2010 at 10:31:34AM +0100, Andrew Coppin wrote:
I have literally no idea what a type family is. I understand ATs (I think!), but TFs make no sense to me.
ATs are just TFs which happen to be associated with a particular class. So if you understand ATs then you understand TFs too, you just didn't know it. =)
How would that make sense though? I'm having trouble forming a mental image of how / why you'd use that...
Type families ---in the traditional dependent-types sense, not necessarily the GHC sense--- are a collection of related types which are "the same" in some sense, but which are distinguished from one another by indices. There are two ways of interpreting this. The first approach is to think about type families where the index gives you some type-level information about the term-level value; this is the same thing as GADTs. That is, if we take the standard whipping boy: data List :: * -> * -> * where nil :: forall a. List a Z cons :: forall a. a -> List a n -> List a (S n) then we'll want some way of talking about "all Lists", irrespective of their lengths. Thus, "List A" (for some A) is a type family, but not a type. There's a fundamental difference here between parametric polymorphism and type indices. In Coq it's made more explicit (though it's still rendered subtle), but in Haskell it can be a bit harder to see. The other perspective is to think of type families as a function from indices to types, where the particular function constitutes the type family. This is the approach taken by associated types and type families in GHC. TFs, as separate from ATs, are useful for implementing type-level functions. For example, we could define addition on Z and S, which would allow us to give the type (++) :: List a n -> List a m -> List a (Plus n m) The type family Plus takes two indices and returns a type, but it does so in a way that it is allowed to perform case analysis on the input arguments--- and therefore is not parametric. -- Live well, ~wren
participants (7)
-
Andrew Coppin -
Brent Yorgey -
Ivan Lazar Miljenovic -
Sjoerd Visscher -
Steffen Schuldenzucker -
Stephen Tetley -
wren ng thornton