On 31 Jan 2009, at 20:54, Gregg Reynolds wrote:

On Sat, Jan 31, 2009 at 1:02 PM, Ben Moseley wrote:

...

You can view a polymorphic unary type constructor of type ":: a -> T" as a polymorphic function.

Shouldn't that be * :: a -> T a ?

Yes, you're right. And when I say "polymorphic unary type constructor" I really mean "polymorphic unary /data/ constructor" ...

...

In general, polymorphic functions correspond roughly to natural transformations (in this case from the identity functor to T).

Are you saying a type constructor is a nat trans and not a functor (component)?

Nope ... what I was trying to say is that the data constructor bit is like a nat trans. (You're right that a unary type constructor often does correspond to a functor - providing there's a corresponding arrow/ function component).

Seems much more like a plain ol' functor mapping of object to object to me - the objects being types. Can you clarify what you mean about the correspondence with natural transformations?

So, the idea is that any polymorphic Haskell function (including Data constructors) can be seen as a natural transformation - so a "function" from any object (ie type) to an arrow (ie function). So, take "listToMaybe :: [a] -> Maybe a" ... this can be seen as a natural transformation from the List functor ([] type constructor) to the Maybe functor (Maybe type constructor) which is a "function" from any type "a" (eg 'Int') to an arrow (ie Haskell function) eg "listToMaybe :: [Int] -> Maybe Int". Hope that makes somewhat more sense. Cheers, --Ben

I admit I haven't thought through "polymorphic function", mainly because there doesn't seem to be any such beast in category theory, and to be honest I've always thought the metaphor is misleading. After all, a function by definition cannot be polymorphic. It seems like fancy name for a syntactic convenience to me - a way to express /intensionally/ a set of equations without writing them all out explicitly.

Thanks,

gregg

...

--Ben

On 31 Jan 2009, at 17:00, Gregg Reynolds wrote:

...

Hi,

I think I've finally figured out what a monad is, but there's one thing I haven't seen addressed in category theory stuff I've found online. That is the relation between type constructors and data constructors.

As I understand it, a type constructor Tcon a is basically the object component of a functor T that maps one Haskell type to another. Haskell types are construed as the objects of category "HaskellType". I think that's a pretty straightforward interpretation of the CT definition of functor.

But a data constructor Dcon a is an /element/ mapping taking elements (values) of one type to elements of another type. So it too can be construed as a functor, if each type itself is construed as a category.

So this gives us two functors, but they operate on different things, and I don't see how to get from one to the other in CT terms. Or rather, they're obviously related, but I don't see how to express that relation formally.

If somebody could point me in the right direction I'd be grateful. Might even write a tutorial. Can't have too many of those.

Thanks,

Gregg _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Sun, Feb 1, 2009 at 12:36 PM, Gregg Reynolds wrote:

On Sat, Jan 31, 2009 at 3:14 PM, David Menendez wrote:

...

There's a paper about defining catamorphisms for GADTs and nested recursive types that models type constructors that way.

If you recall a title or author I'll google it.

I believe it was "Foundations for Structural Programming with GADTs". http://crab.rutgers.edu/~pjohann/popl08.pdf

...

...

So this gives us two functors, but they operate on different things, and I don't see how to get from one to the other in CT terms. Or rather, they're obviously related, but I don't see how to express that relation formally.

Again, what sort of relationship are you thinking of? Data

Ok, good question. I guess the problem I'm having is one of abstraction management. CT prefers to disregard the "contents" of its objects, imposing a kind of blood-brain barrier between the object and its internal structure. Typical definitions of functor, for example, make no reference to the "elements" of an object; a functor is just a pair of morphisms, one taking objects to objects, the other morphisms to morphisms. This leaves the naive reader (i.e. me) to wonder how it is that the internal stuff is related to the functor stuff.

Right. The reason the definition of functor doesn't say anything about the "internal stuff" is that there are plenty of categories where there *is* no internal stuff. So for categories like Set or Mon, where the objects to have elements, category theory uses morphisms to describe their internal structure. For example, a set is an object in Set, and its elements are morphisms from the singleton set. So if I have some operation that creates a monoid from a set, and transforms set functions into monoid homomorphisms in a way that respects identity functions and composition, then I have a functor from Set to Mon. (For example, the free monoid that Wren mentioned.) Whatever internal stuff is going on will be reflected in the morphism part of the functor, because otherwise the functor can't map the morphisms correctly.

For example: is it true that the object component of a functor necessarily "has" a bundle of specific functions relating the internal "elements" of the objects? If so, is the object component merely an abstraction of the bundle? Or is it ontologically a different thing?

Let me try to give an illustrative example. Consider a category A with a single object and a bunch of morphisms from that object to itself. Now, the object itself isn't interesting, which is why I didn't give it a name. It's not any kind of set, and the morphisms aren't functions: composition just combines them in some unspecified manner. Because A is a category, we know that there's an identity morphism id, such that f . id = f = id . f, and we know that f . (g . h) = (f . g) . h. In other words, the morphisms in a single-object category form a monoid. What's more, since we don't care about what the morphisms are, we can take any monoid and create a single-object category. For example, we could define a category Plus where the morphisms are natural numbers, the identity morphism is 0, and morphism composition is addition. Now let's say we have to single-object categories, A and B, and a functor F : A -> B. What do we know about F? We know that F maps the object in A to the object in B, and it maps the identity morphism in A to the identity morphism in B, and that for any morphisms f and g in A, F(f) . F(g) = F(f . g). In other words, F is a monoid homomorphism (that is, a mapping from one monoid to another that respects the identity and the monoid operation). We can define other functors, too. For example, a functor P : Plus -> Set. We'll map the object in Plus to N (the set of natural numbers), and every morphism n in Plus to a function (\x -> n + x) : N -> N. You can prove for yourself that P(0) gives the identity morphism for N, and that P(m + n) = P(m) . P(n). So P is a functor whose object component doesn't have a bundle of specific functions relating the internal elements of the objects. All the interesting stuff in P takes place in the morphism map. Does that help at all? (A side note: As I said, for any monoid X, we can create a category C(X), and it's obvious that for any monoid homomorphism f : X -> Y, we can create a functor C(f) : C(X) -> C(Y). It turns out that for any monoids X, Y, and Z and homomorphisms f : Y -> Z and g : X -> Y, C(f) . C(g) = C(f . g). So C is a functor from the category of monads to the category of categories.) -- Dave Menendez http://www.eyrie.org/~zednenem/

Gregg Reynolds wrote:

On Sat, Jan 31, 2009 at 4:26 PM, wren ng thornton wrote:

...

...

But a data constructor Dcon a is an /element/ mapping taking elements (values) of one type to elements of another type. So it too can be construed as a functor, if each type itself is construed as a category.

Actually no, it's not a functor. It's a (collection of) morphism(s). Let's again assume a single-argument Dcon for simplicity. The Haskell type |Dcon :: forall a. a -> Tcon a| is represented by a collection of morphisms |Dcon_{X} : X -> Tcon X| for each X in Ob(Hask).

Ok, I see I elided that step. So my question is about the relation between the individual (specialized) Dcon and the associated Tcon. I.e. Dcon 3 is a value of type Tcon Int, inferred by the type system. So it looks to me like the relation between the Tcon functor and the Dcon functions is basically ad hoc.

Pretty much. Well, it's not ad hoc, it's algebraic. Data constructors, by definition, don't perform any sort of introspection on the values they're given. Looking at it sideways, they're 'polymorphic' in the values of the type, and they preserve the structure of the value (namely just storing it). This makes data constructors more well behaved than arbitrary functions. The possible definitions of Haskell types are formed by the algebra consisting of that id function, products of algebras, coproducts of algebras, and equi-recursion (though removing this and using iso-recursion is easier for CT treatment). This well-behavedness is without even looking at polymorphic data constructors. To take a different tactic, consider the free monoid. Like all free things it is the monoid which consists of no more than what is necessary to satisfy the monoid laws (that is, it doesn't cost or require anything special; hence "free"). If you're familiar with Prolog, this is like the idea of uninterpreted predicates. The value of foo(bar) is: foo(bar). Since foo is uninterpreted, applying foo to bar means returning a value that reifies the application of foo to bar. Uninterpreted predicates are "free application"[1]. Data constructors in Haskell are just like this. Applying (:) to x and xs results in the value (x:xs). It is precisely because Dcons cannot inspect the values they are given that makes it so easy for Tcons to be functors. Since the only thing Dcons can do to values is id them up, this is definitionally structure preserving. Note that it's possible to have functors which do inspect the values but still preserve structure by transforming the values in some consistent manner. Because Dcons cannot do anything, this is why people often define "smart" constructors for dealing with abstract types or for maintaining invariants in types which have more structure than can be encoded in ADTs (or GADTs). For example, the bytestring-trie package defines a Trie type for patricia trees mapping ByteStrings to some value type. The basic type for Trie a has Empty, Arc :: ByteString -> Maybe a -> Trie a, and Branch :: Trie a -> Trie a -> Trie a. However, the actual abstract type has a number of invariants which restrict the domain of the type to be much smaller than what you would get with just that specification (e.g. an Arc with no value can't recurse as an Arc, the arcs should be collapsed into one). Smart constructors are an important technique and they can capture many interesting types which ADTs cannot, however when using smart constructors you've stepped outside of the warm confines of what the type system enforces for you. The Haskell type Trie a is not the same thing as the abstract type it's used to represent. By stepping outside of the type system, it's up to the programmer to prove that their abstract type does adhere to the laws for functors, monoids, or whatever. For ADTs, those proofs are already done for you (for functors at least) due to their regular nature. And I do mean "regular", ADTs are coproducts, products, and recursion just like the choice, extension, and Klene star of regular expressions. [1] Easing off from the free monoid, the free associative operator is free (binary) application extended by an equivalence relation for associativity. Thus, values generated by the free assoc-op represent equivalence classes over the application trees which could generate it. The free monoid is the same thing but extended by equivalence relations for the identity element (which is often written by writing nothing, hence it's also an equivalence relation over all possible insertions of the identity element).

...

It's important to remember that Tcon is the object half of an *endo*functor |Tcon : Hask -> Hask| and not just any functor. We can view the object half of an endofunctor as a collection of morphisms on a category; not necessarily real morphisms that exist within that category, but more like an overlay on a graph. In some cases, this overlay forms a subcategory (that is, they are all indeed morphisms in the original category). And this is what we have with data constructors: they are (pieces of) the image of the endofunctor from within the category itself.

(unknotting arms...) Uh, er, hmm. I'm still having abstraction vertigo, since we have (I think) data constructors qua generic thingees that work at the level of the category, and the same, specialized to a type, qua functions that operate on the internals of the categorical objects. It's the moving back and forth from type and value that escapes me, and I'm not sure I'm even describing the issue properly. I shall go away and thing about this and then write the answer down.

It won't help the vertigo any, but we can tune the level of abstraction in a few more ways. With some hand waving: * A type constructor is a bundle of polymorphic functions. * A polymorphic function is a bundle of monomorphic functions. * A monomorphic function is a bundle of unit functions (that is, functions from one specific value of the domain "value bundle" (aka "type"), to one specific value of the codomain's "value bundle"). In some ways each of these levels are similar to the others in terms of how they bundle things together so as to be "structure preserving" in the necessary ways. But in some ways, each of the levels are different in what it means to be "bundled". As you say, category theory does it's best to ignore what goes on inside of objects, instead it's all about what goes on between objects (and anything inside of objects is merely "structure" to be preserved). Set theory and domain theory tend to focus more on what goes on inside. Perhaps the simplest way to think of the relation is that the Tycon perspective yields a functor, whereas the Dcon perspective yields a natural transformation (eta : Id -> F, for some endofunctor F). I started writing up a post about this earlier in the context of polymorphic functions being natural transformations. But general polymorphic functions have some extra fiddly details that obscure the message (hence not sending the mail). For type constructors, though, it's straightforward. I'm guessing that your intuitions about the fact that there's stuff happening on multiple levels is coming from the natural transformation. The first few times you run into them, they tend to have that disorienting effect. Part of this disorientation, I think, stems from the fact that natural transformations are structure-preserving transformations from structure-preserving transformations to structure-preserving transformation (say what?). This shouldn't be that mindboggling since we frequently talk about functions from functions to functions (e.g. fmap_{F} :: (a -> b) -> (F a -> F b)), but the level of abstraction can make it difficult to pin down. Personally, I think the confusion is compounded by the way most CT tutorials introduce natural transforms. Usually they start with something like "this is a category", then move onto "this is a functor", then they say that functors are also morphisms in the category, Cat, of small categories; which is all good. (And already we have the morphism/functor and object/category vertigo.) But then, when explaining natural transformations they say something about them being "like functors but moreso", then everything comes crashing down because that often gets people visualizing functors on categories of categories, but those are just functors too. If we're looking at Cat, and we pick two objects X and Y (aka categories C and D), and then pick two morphisms f and g (aka functors F and G), a natural transformation is a structure preserving transformation from f into g. A key difference between this and a functor on Cat is that X and Y are fixed; we do not say "for all X, Y, and f : X->Y" like we would for a functor. YMMV, and all that. -- Live well, ~wren

On Sat, Jan 31, 2009 at 5:11 PM, Derek Elkins wrote:

...

But a data constructor Dcon a is an /element/ mapping taking elements (values) of one type to elements of another type. So it too can be construed as a functor, if each type itself is construed as a category.

What are "elements" of a type? How are you "construing a type as a category"? One answer is that you are viewing types as sets. Ignoring

That's a good question. I've been hoping that viewing types as sets is good enough but that doesn't seem to be the case.

Most articles that apply CT to Haskell take one of two approaches. They either talk about a category of Haskell types and functions with no explanation of what those "actually" are, i.e. the understanding that it behaves like (idealized) Haskell, or they refer to some existing approach to (idealized) semantics, e.g. sets or domains. In either case, the meaning of the objects and arrows is effectively taken for granted.

You can say that again.

An approach along the lines you are suggesting would be useful for a categorical semantics of Haskell, but it would just be one possible semantics among many. For most of the aforementioned articles, the only value of such a thing would be to be able to formally prove that the constructions talked about exist (except that they usually don't for technical reasons.) Usually in those articles, the readers are assumed to know Haskell and to not know much about category theory, so trying to explain types and functions to them categorically is unnecessary and obfuscatory. It would make sense if you were going the other way, explaining Haskell to categorists.

Actually, what I have in mind using the concepts and terminology of CT to explain Haskell to ordinary programmers. The idea is not necessarily to prove stuff, but to build the intuitions needed to think about computing at a higher level of abstraction before proceeding to Haskell. I suspect this might be the quicker road to Haskell mastery; even if not it's a fun writing project. Call me nutty, but I think the basic concepts of CT - category, functor, natural transformation, monad - are actually pretty simple, even though it took much gnashing of teeth for me to acquire a basic intuition. You don't have to be a mathematician to see the basic structural ideas and get some idea of their usefulness, /if/ you have appropriate pedagogical material. Alas, I've found that clear, simple explanations are scattered across lots of different documents. Thanks for your help; I can see I've got a few more things to work on (like "type"). -gregg