Constraints on definition of `length` should be strengthened

[Edward Kmett]

In that code, I made a more powerful version of Functor that can handle
more interesting categories.

In that setting, the fact that we use 'curried' types matters quite a bit.
The usual way to think of a bifunctor is as a functor from a product
category, which would like like something of kind (*,*) -> *. And you can
define such a beast in Haskell. The "truly unbiased" tuple some folks have
been hollering for in this thread would ideally have this sort of kind.
After all, then it can't be Foldable, Traversable, etc.

In
http://hackage.haskell.org/package/semigroupoid-extras-5/docs/Data-Semifunctor.html
Bi (,) and Bi Either provide these semantics today.

But in this more general setting where we can have Functors that go to
other categories than just Hask, haskell's "Bifunctor", which has kind * ->
* -> * is a functor that to a functor category. We can curry/uncurry the
kinds involved to go back and forth between these two representations and
that always works in a category that is locally small like what we can
define in Haskell. 'Bi' is a form of type level uncurry.

In the hask code, Either is a functor from Hask to [Hask,Hask], where the
latter is the category of functors from Hask -> Hask.
This of course, fundamentally relies on the fact that Either a being a
Functor. Mutatis mutandis for (,) a being a functor.

Once you have those things you can use runNat from the package in question
to move 'backwards' n arguments an:d map over any field you want, be it a
bifunctor, trifunctor, whatever. Contravariant becomes a functor from an
opposite category, and large numbers of classes we have just collapse away
into one thing: Functor.

Bifunctor ceases to be a primitive notion and just becomes a derived fact
from the existence of those two Functor instances.

I find this to be far more enlightening than a arbitrarily adopting an
unbiased (,) and making the entire world adopt mutually incompatible data
types. YMMV.

-Edward

On Sun, Apr 9, 2017 at 12:42 PM, <dominic at steinitz.org> wrote:

> I am not sure what to make of the “documentation” to which you refer. For
> example, a type Tensor seems to be defined. Now you can tensor lots of
> things with some algebraic structure but most commonly vector fields and
> modules (modules in the mathematical sense that is). The type Tensor seems
> to have no relation to these and there is no prose giving an indication of
> the author’s intent. Perhaps we should be cautious about adducing other
> parts of the package as evidence?
>
> > Already done mate.
> >
> > https://hackage.haskell.org/package/hask-0/docs/Hask-
> Category.html#t:Either
> > https://hackage.haskell.org/package/hask-0/docs/Hask-
> Category.html#t:Functor
> >
> > Note the multiple Functor instances for Either and Coproduct. e.g.
> >
> > - Functor * (* -> *) Either
> > - Functor * * (Either a)
> > etc etc
> >
> > On 09/04/17 10:29, Henrik Nilsson wrote:
> >> And of course, if, in a hypothetical future version of Haskell
> >> where we could make all possible functor instances for tuples,
> >> the question becomes: which one do we pick? The answer might well
> >> be "none" (in the prelude, at least).
>
> Dominic Steinitz
> dominic at steinitz.org
> http://idontgetoutmuch.wordpress.com
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20170410/c56599ee/attachment-0001.html>