4 ms·

I'm confused by his argument that Haskell functors are only endofunctors because everything is Hask. I thought that even if everything is part of one category,

I'm confused by his argument that Haskell functors are only endofunctors because everything is Hask. I thought that even if everything is part of one category, if the input is a different category that is a subset of the one category and transformed to another category, even if a subset of the same category, it could still be a regular functor instead of an endofunctor. For example, lets say you had a function f(x) that takes unsigned ints and returns the signed int inverse (so f(1) = -1). -1 is not part of the unsigned category since it is below the Initial value of an unsigned number (0). I'm a total newbie to category theory so I'm not sure if he's wrong or I'm missing a key detail here.

contravariant 4y ago
You could probably try to talk about functors between subcategories by using classes, though I think there's no way to define a functor from one class to another in Haskell. Slightly more annoying is the fact that Haskell has no real product types and instead does more currying than an Indian takeaway. This makes various constructions in Category theory a bit more annoying than they need to be. If you ever wondered what on earth Applicable is and why you need it to fmap a function with multiple arguments, this is why. There's also the fact that Haskell doesn't really enforce the functor laws, nor does it give any way to really state them. Basically it uses Category theory as a close enough approximation for what it does, but various finer details get lost in translation.
- runevault 4y ago
  Okay this gives me something to go on, thanks!
- Y_Y 4y ago
  Haskell isn't the functor police! It's on you to define good functors, proving them so would be a totally different endeavour and far more difficult. I would like to understand better the issue with product types though. What do you want to do that you can't currently. By the way, most of my knowledge about the connection between Haskell and Category Theory comes from here: https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
  - gowld 4y ago
    What is an example of category-theory functor in Haskell, that isn't just an endofunctor? A functor F from C to D is a mapping that associates each object X in C to an object F(X) in D. In Haskell, C and D are both the same (Hask types), hence endofunctor (functor into self). In general a functor could be something like `prime_factorizaton:: Int -> [(Prime Int, Mulitplicity Int)]`, with morphisms being things like the operation a => square :: a -> a square (n::Integer) = n^2 square (factorization::[(Prime Int, Mulitplicity Int)]) = map (\(a,b) -> (a, 2*b))) prime_factorizaton (square) x === square (prime_factorization(x))
    - Iceland_jack 4y ago
      Either a :: Type -> Type is a Haskell Functor (endofunctor), mapping (->) to (->). Either :: Type -> (Type -> Type) is not an endofunctor, it maps a type to a type constructor and thus maps (->) to (~>) (natural transformations). If you uncurried Either, you would also get a non-endofunctor which maps from (-×>) (product category) to (->). Either' :: (Type, Type) -> Type Every function is a functor between equality, since equality satisfies congruence: isPrime :: Integer -> Bool is a functor between (:~:) @Integer an (:~:) @Bool. Boolean negation is a function between "less than or equal" to "greater than or equal" categories; mapping (<=) to (>=): not :: Bool -> Bool
  - contravariant 4y ago
    Hmm, well calling it a problem might be a bit much, but it means that functions with more than argument require some additional care, and technically a stronger notion of functor. Say you have a multivariate function a: X x Y -> Z, and a functor F. This would give you a function F(a): F(X x Y) -> F(Z). Now this is not really multivariate any more as F(X x Y) is not a product, but products behave quite well in category theory so this is not usually that big a problem, and it turns out that quite a few functors are 'continuous' which means they preserve 'limits' and a product is one such limit, in which case F(X) x F(Y) ~= F(X x Y). In particular all right adjoint functors have this property, which is why adjointness is such an important concept. Now in Haskell things get slightly more difficult, because you don't have a function a: X x Y -> Z, you've got a function a: X -> (Y => Z). Where Y => Z is an object representing all maps from Y to Z (such an object may or may not exist for any particular category). And to use currying you need something like (X * Y) -> Z and X -> (Y => Z) to be isomorphic. So you don't just need F(X x Y) = F(X) x F(Y), which is fairly innocuous, you need to deal with monoidal categories and monoidal functions between them, which is a heck of a lot more complex. This is where the Applicative stuff comes from. Now some of the stuff you don't get as easily in Haskell is the stuff relying on basic properties of sum and product types, such as # The following are the obvious projections for a 2-tuple proj1 :: (X x Y) -> X proj2 :: (X x Y) -> Y # Assuming F(X) x F(Y) exists we get the following for free (F(proj1) x F(proj2)) :: F(X x Y) -> F(X) x F(Y) No clue how you'd state that in Haskell. And the following # The following are the obvious projections for a 2-tuple anX :: X -> (X + Y) anY :: Y -> (X + Y) # Assuming F(X) + F(Y) exists we get the following for free (F(anX) + F(anY)) :: F(X) + F(Y) -> F(X + Y) where you can interpret X + Y as an 'Either X Y'. Sure you could probably write a function forall Functor f. Either (f a) (f b) -> f (Either a b) but it's not that obvious that it should exist, whereas in category theory it's one of the most obvious constructions imaginable and its existence is clear from the definition. And in Haskell you wouldn't think about using products so the first property is probably barely used anywhere (there's probably a right inverse for zip somewhere: unzip :: [(a,b)] -> ([a],[b]) but Haskell generally doesn't seem to like functions with multiple outputs.
dwohnitmok 4y ago
I believe the heart of what you're asking is "why do we distinguish between codomain and range?" and relatedly why do we even need the concept of "surjectivity?" For example, the function f(x) = x + x could be thought of a non-surjective "endo-"function (endomorphism) `N -> N` (where N is the natural numbers) or it could be thought of as a surjective function from `N -> E` (where E is the even natural numbers). Why do we need the "looser" version of `N -> N` when we can do with the tighter bound `N -> E`? As with many definitional things in pure mathematics, the answer is "there's no absolute iron-clad reason why you can't think of things that way, but there are a variety of reasons both mechanistic and motivated by intuition why you might not want to do that." To motivate it via intuition, let me start with another example. Take the function that maps every natural number k to the function f(x) = x + k (so it's a function whose codomain is `(N -> N)` or also expressed as `N^N`, allowing again for the fact that N^N is again "too loose" since we only care about functions of the form f(x) = x + k). Now someone could come along and say "well, f(x) = x + k" can be simply identified with just k so really the function we have is the identity function on `N -> N`, but I think most people would object and say that `k` is not the same thing as `f(x) = x + k`. The former can be thought of as an encoding of the latter, but it's not the same thing. So saying that the codomain of our function is N^N is in some sense more accurate than N and instead we can say that there's a way of embedding a subset of N^N into N via encoding f(x) = x + k as just k. The crucial thing here is that deciding whether we are dealing with an artificial encoding of something, or the real thing itself is what lets us distinguish between saying that the function's codomain is N vs N^N, and in some sense the former feels "wrong" even though it's a "tighter bound." Let's develop that intuition a little bit further. Imagine you have a function that takes a rational number and maps it to the largest integer smaller than it (that is the floor function). You could think of this function in one of at least four ways: 1. Q -> Q: A function that maps a rational number back to a rational number 2. Q -> Z: A function that maps a rational number to an integer 3. Z -> Z: Because rational numbers are countable, every rational number is "just" the indexed form of an integer, so "really" what we have is a function from Z -> Z 4. N -> N: Well by the same logic, every function on integers is just a function on natural numbers! I think the last two probably feel the most "unnatural" for folks, and most representative of the problem of "representation vs what an object 'really' is" I talked about earlier. But the first two have what is basically the same choice, just in a context where the answer isn't as clear. Do you think the integer 2 really is just the same number as the rational number "2 / 1?" Or do you think that they are different from each other and an encoding process is necessary to move from one to the other? In some cases it's useful to say "yes every integer is exactly a rational number" and in that case we can say that Q -> Q reflects this intuition best. In other cases it might be more useful to say "no an integer is not a rational number, but there is a canonical way of identifying every integer with a certain rational number" and in that case we can say that Q -> Z reflects that intuition. So your choice of codomain reflects what you think an object "really is" as opposed to just being an encoding. In this case we say that choosing Hask as the codomain (or "target") of our functor, hence making it an endofunctor, is a choice that reflects an intuition that the result of mapping using a Haskell functor is really just another type, not some other object that can be thought of as a type. From this intuition there flows a variety of practical, mechanistic ramifications. Almost always when talking about mappings we are concerned about how they affect the structure of the source and target. When we say the codomain is the same as the domain, we also almost always mean that structurally they are the same and this considerably simplifies the analysis we need to do later, because we can reuse a lot of the same machinery in the domain and codomain. If you say that the codomain and domain are not the same, then all of a sudden you have to concern yourself with the structure of the codomain and domain and prove that all the equivalences and isomorphisms you want to hold and preserve the properties you care about do actually exist and do actually preserve everything you want preserved and it's just a lot more annoying. So at a mechanistic level, what we gain from saying that "Haskell functors are only endofunctors because everything is Hask" is that we know we never map into something that has more structure than Hask; it always has the same structure. So we don't have to concern ourselves with a bunch of exploration into what happens if we map into a category with more structure than Hask.

contravariant 4y ago

You could probably try to talk about functors between subcategories by using classes, though I think there's no way to define a functor from one class to another in Haskell. Slightly more annoying is the fact that Haskell has no real product types and instead does more currying than an Indian takeaway. This makes various constructions in Category theory a bit more annoying than they need to be. If you ever wondered what on earth Applicable is and why you need it to fmap a function with multiple arguments, this is why. There's also the fact that Haskell doesn't really enforce the functor laws, nor does it give any way to really state them. Basically it uses Category theory as a close enough approximation for what it does, but various finer details get lost in translation.

runevault 4y ago
Okay this gives me something to go on, thanks!
Y_Y 4y ago
Haskell isn't the functor police! It's on you to define good functors, proving them so would be a totally different endeavour and far more difficult. I would like to understand better the issue with product types though. What do you want to do that you can't currently. By the way, most of my knowledge about the connection between Haskell and Category Theory comes from here: https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
- gowld 4y ago
  What is an example of category-theory functor in Haskell, that isn't just an endofunctor? A functor F from C to D is a mapping that associates each object X in C to an object F(X) in D. In Haskell, C and D are both the same (Hask types), hence endofunctor (functor into self). In general a functor could be something like `prime_factorizaton:: Int -> [(Prime Int, Mulitplicity Int)]`, with morphisms being things like the operation a => square :: a -> a square (n::Integer) = n^2 square (factorization::[(Prime Int, Mulitplicity Int)]) = map (\(a,b) -> (a, 2*b))) prime_factorizaton (square) x === square (prime_factorization(x))
  - Iceland_jack 4y ago
    Either a :: Type -> Type is a Haskell Functor (endofunctor), mapping (->) to (->). Either :: Type -> (Type -> Type) is not an endofunctor, it maps a type to a type constructor and thus maps (->) to (~>) (natural transformations). If you uncurried Either, you would also get a non-endofunctor which maps from (-×>) (product category) to (->). Either' :: (Type, Type) -> Type Every function is a functor between equality, since equality satisfies congruence: isPrime :: Integer -> Bool is a functor between (:~:) @Integer an (:~:) @Bool. Boolean negation is a function between "less than or equal" to "greater than or equal" categories; mapping (<=) to (>=): not :: Bool -> Bool
- contravariant 4y ago
  Hmm, well calling it a problem might be a bit much, but it means that functions with more than argument require some additional care, and technically a stronger notion of functor. Say you have a multivariate function a: X x Y -> Z, and a functor F. This would give you a function F(a): F(X x Y) -> F(Z). Now this is not really multivariate any more as F(X x Y) is not a product, but products behave quite well in category theory so this is not usually that big a problem, and it turns out that quite a few functors are 'continuous' which means they preserve 'limits' and a product is one such limit, in which case F(X) x F(Y) ~= F(X x Y). In particular all right adjoint functors have this property, which is why adjointness is such an important concept. Now in Haskell things get slightly more difficult, because you don't have a function a: X x Y -> Z, you've got a function a: X -> (Y => Z). Where Y => Z is an object representing all maps from Y to Z (such an object may or may not exist for any particular category). And to use currying you need something like (X * Y) -> Z and X -> (Y => Z) to be isomorphic. So you don't just need F(X x Y) = F(X) x F(Y), which is fairly innocuous, you need to deal with monoidal categories and monoidal functions between them, which is a heck of a lot more complex. This is where the Applicative stuff comes from. Now some of the stuff you don't get as easily in Haskell is the stuff relying on basic properties of sum and product types, such as # The following are the obvious projections for a 2-tuple proj1 :: (X x Y) -> X proj2 :: (X x Y) -> Y # Assuming F(X) x F(Y) exists we get the following for free (F(proj1) x F(proj2)) :: F(X x Y) -> F(X) x F(Y) No clue how you'd state that in Haskell. And the following # The following are the obvious projections for a 2-tuple anX :: X -> (X + Y) anY :: Y -> (X + Y) # Assuming F(X) + F(Y) exists we get the following for free (F(anX) + F(anY)) :: F(X) + F(Y) -> F(X + Y) where you can interpret X + Y as an 'Either X Y'. Sure you could probably write a function forall Functor f. Either (f a) (f b) -> f (Either a b) but it's not that obvious that it should exist, whereas in category theory it's one of the most obvious constructions imaginable and its existence is clear from the definition. And in Haskell you wouldn't think about using products so the first property is probably barely used anywhere (there's probably a right inverse for zip somewhere: unzip :: [(a,b)] -> ([a],[b]) but Haskell generally doesn't seem to like functions with multiple outputs.

dwohnitmok 4y ago

I believe the heart of what you're asking is "why do we distinguish between codomain and range?" and relatedly why do we even need the concept of "surjectivity?" For example, the function f(x) = x + x could be thought of a non-surjective "endo-"function (endomorphism) `N -> N` (where N is the natural numbers) or it could be thought of as a surjective function from `N -> E` (where E is the even natural numbers). Why do we need the "looser" version of `N -> N` when we can do with the tighter bound `N -> E`? As with many definitional things in pure mathematics, the answer is "there's no absolute iron-clad reason why you can't think of things that way, but there are a variety of reasons both mechanistic and motivated by intuition why you might not want to do that." To motivate it via intuition, let me start with another example. Take the function that maps every natural number k to the function f(x) = x + k (so it's a function whose codomain is `(N -> N)` or also expressed as `N^N`, allowing again for the fact that N^N is again "too loose" since we only care about functions of the form f(x) = x + k). Now someone could come along and say "well, f(x) = x + k" can be simply identified with just k so really the function we have is the identity function on `N -> N`, but I think most people would object and say that `k` is not the same thing as `f(x) = x + k`. The former can be thought of as an encoding of the latter, but it's not the same thing. So saying that the codomain of our function is N^N is in some sense more accurate than N and instead we can say that there's a way of embedding a subset of N^N into N via encoding f(x) = x + k as just k. The crucial thing here is that deciding whether we are dealing with an artificial encoding of something, or the real thing itself is what lets us distinguish between saying that the function's codomain is N vs N^N, and in some sense the former feels "wrong" even though it's a "tighter bound." Let's develop that intuition a little bit further. Imagine you have a function that takes a rational number and maps it to the largest integer smaller than it (that is the floor function). You could think of this function in one of at least four ways: 1. Q -> Q: A function that maps a rational number back to a rational number 2. Q -> Z: A function that maps a rational number to an integer 3. Z -> Z: Because rational numbers are countable, every rational number is "just" the indexed form of an integer, so "really" what we have is a function from Z -> Z 4. N -> N: Well by the same logic, every function on integers is just a function on natural numbers! I think the last two probably feel the most "unnatural" for folks, and most representative of the problem of "representation vs what an object 'really' is" I talked about earlier. But the first two have what is basically the same choice, just in a context where the answer isn't as clear. Do you think the integer 2 really is just the same number as the rational number "2 / 1?" Or do you think that they are different from each other and an encoding process is necessary to move from one to the other? In some cases it's useful to say "yes every integer is exactly a rational number" and in that case we can say that Q -> Q reflects this intuition best. In other cases it might be more useful to say "no an integer is not a rational number, but there is a canonical way of identifying every integer with a certain rational number" and in that case we can say that Q -> Z reflects that intuition. So your choice of codomain reflects what you think an object "really is" as opposed to just being an encoding. In this case we say that choosing Hask as the codomain (or "target") of our functor, hence making it an endofunctor, is a choice that reflects an intuition that the result of mapping using a Haskell functor is really just another type, not some other object that can be thought of as a type. From this intuition there flows a variety of practical, mechanistic ramifications. Almost always when talking about mappings we are concerned about how they affect the structure of the source and target. When we say the codomain is the same as the domain, we also almost always mean that structurally they are the same and this considerably simplifies the analysis we need to do later, because we can reuse a lot of the same machinery in the domain and codomain. If you say that the codomain and domain are not the same, then all of a sudden you have to concern yourself with the structure of the codomain and domain and prove that all the equivalences and isomorphisms you want to hold and preserve the properties you care about do actually exist and do actually preserve everything you want preserved and it's just a lot more annoying. So at a mechanistic level, what we gain from saying that "Haskell functors are only endofunctors because everything is Hask" is that we know we never map into something that has more structure than Hask; it always has the same structure. So we don't have to concern ourselves with a bunch of exploration into what happens if we map into a category with more structure than Hask.