Add monomorphic classes for * alongside existing ones for * → *

[liyang]

Current classes in linear are only instantiable for * → * kinds. We'd be able to supplant vector-space had we classes for * kinds as well.

Preliminary discussion on #haskell-lens; @acowley @ekmett @shachaf

[dmcclean]

This is an interesting proposal/discussion.

Could monomorphic classes coexist with polymorphic classes? Either with the monomorphic ones superclasses of the polymorphic ones or with an opt-in once-and-for-all (potentially-)overlapping instance of the monomorphic ones in terms of the polymorphic ones?

Having the coexisting lerp and affine space operators is confusing in modules that need both.

My use for monomorphic classes isn't performance when specialized to Double, it's types that represent various notions of time. Although now that I am thinking about it "out loud" I wonder if I can just rearrange my time types to be polymorphic and then use type synonyms to hide it in places that don't need to be concerned with it...., so I'm going to go investigate that.

[dmcclean]

Hmm. Almost.

The sticking point is the Functor superclass requirement on Additive. I can't make dimensional-dk's Quantity d (where d is a phantom type representing a physical dimension), which I wish to make Additive, an instance of Functor because if I did people could fmap under the units and do nonsense things, mostly defeating the point.

After browsing the source (of just the Linear.Vector module, not of the whole package, so this may be the tip of the iceberg) it looks like the reason for this constraint it twofold. First it is used to define negation and subtraction, second it's very convenient for lots of other things that would otherwise need a more verbose constraint.

In contrast the Data.AdditiveGroup module has the negation function inside the typeclass and doesn't define a default implementation. (It also has the subtraction function defined in the obvious way in terms of negation, but outside the typeclass.)

[bergey]

If diagrams were to use linear, we'd have a similar problem to @dmcclean's. Our Angle type should hide whether it is represented by radians, degrees, or something else, and fmap (with suitably chosen function) does too much.

It's probably OK to trust users not to do nonsense like fmap (\x -> x*x) (180 degrees), but I'd be interested in seeing a design for monomorphic Additive for this sort of thing. I can't promise that I have time to work on it, though.

More discussion: http://ircbrowse.net/browse/diagrams?events_page=1512

[ekmett]

The main hazard I see with 'monomorphic Additive' is what does it mean to multiply a matrix in that world?

We have matrix multiplication as:

(!*!) :: ... => m (t a) -> t (n a) -> m (n a)

Every proposal I've seen has led to situations where you have some vector spaces that can only occur on the 'right hand side' of a matrix.

That is many things, but its not a vector space. ;)

[dmcclean]

One thing I was thinking about the other day was that I ran into a type like:

data Atmos a = Atmos { atmosTemperature :: a
, atmosPressure :: a
, atmosDensity :: a
, atmosSpeedOfSound :: a
, atmosViscosity :: a
, atmosKinematicViscosity :: a
}

Where you could have a Functor instance. But when you get to the dimensional version of it:

data Atmos a = Atmos { atmosTemperature :: ThermodynamicTemperature a
, atmosPressure :: Pressure a
, atmosDensity :: Density a
, atmosSpeedOfSound :: Velocity a
, atmosViscosity :: DynamicViscosity a
, atmosKinematicViscosity :: KinematicViscosity a
}

you run into a different version of the same thing. And thus I couldn't match the Functor g context in jacobian :: (Traversable f, Functor g, Num a) => (forall s. Reifies s Tape => f (Reverse s a) -> g (Reverse s a)) -> f a -> g (f a).

So maybe what's actually wanted isn't monomorphic vector spaces but weaker functors. Functors that only can fmap functions that are in some vague sense "identityish" in that they change the representation of a number but don't change what number it is.

Since this is (a) (hopelessly?) vague, (b) undecidable, and (c) in a package depended on by the entire universe, it seems like the best thing to do is probably to stop worrying and love the bomb.

Or maybe this, which limits the scope in which you are willing to love the bomb:

newtype UnsafeQuantity d a = UnsafeQuantity (Quantity d a)

instance Functor (UnsafeQuantity d) where
  fmap = -- unwrap it, trust the supplied function, and wrap it again

[bergey]

I agree - if I don't make my types Functor, I'm going to need to define something with a different name but the same behavior, to use realToFrac inside the type. So I'm convinced to "love the bomb" as you say.

[dmcclean]

Thinking about it again, there's a way you can look at it that makes this problem the same as the dreaded "restricted monad"/"how do I make Data.Set a monad" question.

Adopting the Functor version of the ConstraintKinds solution to the restricted monad problem:

class RFunctor f where
  type RFunctorCtxt f a :: Constraint
  fmap :: (RFunctorCtxt f a, RFunctorCtxt f b) => (a -> b) -> f a -> f b

You could have

instance RFunctor (Quantity d) where
  type RFunctorCtxt (Quantity d) a = (Real a)
  fmap _ (Quantity x) = Quantity (fromRational $ toRational x)

Even though its implementation of fmap completely ignores the function being mapped, it still respects the functor laws (assuming the Real instance(s) is/are well behaved).

This formalizes what I meant by "functions that are in some vague sense "identityish" in that they change the representation of a number but don't change what number it is" and ensures that we only fmap those functions.

Not worth doing, but interesting to think about.

[ekmett]

This has come up as a proposed solution before, but "restricted functors" get in the way of building things like jets of derivatives using linear, and you lose the fact that the second functor law follows from the first via parametricity, etc. the cure is worse than the disease IMHO.

[dmcclean]

There's little doubt that it's way worse than the disease, that's for sure.

Especially because I can't see how to recover the ordinary Functor in terms of RFunctor. You need a way to say that RFunctorCtxt f a ~ () that is universally quantified over a, and I don't think we have a weapon that does that, so you can't write a constraint synonym like type Functor f = forall a.(RFunctor f, RFunctorCtxt f a ~ ())

I don't understand the comment about jets of derivatives, but it's probably because I don't understand what a jet is.

[ekmett]

The way I formulate it in AD:

data Jet f a = a :- Jet f (f a)

which looks something like

a :- f a :- f (f a) :- f (f (f a)) :- ...

[ekmett]

It is basically an 'unzipped cofree comonad'.

You can go from Cofree f a to Jet f a for any functor f, but going back isn't always possible (except for representable functors).

[dmcclean]

That's cool. So the idea is that whatever f is structuring the results of your function, you can still build higher order derivatives because you can keep replicating the structure.

Which you couldn't do with restricted functors, basically for the reason that you can't express the constraint that a restricted functor is "ordinary" (in the sense that the context it's restricted to is always ()).

[ekmett]

Technically its the f that was structuring the inputs to your function. you wind up (basically) computing

grads :: (f AD -> AD) -> Jet f Double
jacobians :: (f AD -> g AD) -> g (Jet f Double)

When I figured that out was a bit of an 'aha!' moment for me, and it maps back onto the limit of the notion of an n-jet of derivatives in mathematics as n goes to infinity.

[dmcclean]

I think I see.

So you actually need an even weaker property. You don't need a restricted functor that has context () for all types, you need one where (RFunctorCtxt f a) entails (RFunctorCtxt f (f a)), which is even less encodable into GHC-Haskell.

[ekmett]

Yes, but that is just one particular polymorphically recursive case. I have EDSLs that happen to use others. I basically view the 'restricted monad encoding' as a bad abstraction because it leaks all information about what intermediate steps you pass through into your types and renders things that were once canonical into merely one path through the minefield of unusable types.

[dmcclean]

Indeed. It's weird because these rock/hard-place situations are pretty uncommon in haskell. It seems like you either have to (a) leak the constraint and propagate them everywhere or (b) leak the representation you are using for your units and lose scale invariance. It doesn't even seem like having a more refined typeclass hierarchy than the Num situation would help, either.

Strangely this is one situation where I actually miss having escape hatches from parametricity. In C# land I would think about adding the fmap equivalent and then use reflection to inspect the types I am actually being asked to fmap between and either construct the appropriate conversion function or raise an exception saying that there isn't on. This gives the static appearance that everything is fine, but can't actually be used to build "unsafe" programs that don't explode the first time they are run; you are kept up at night by the possibility that someone only breaks the rules in some extremely unusual scenario that won't be caught in testing, but doing that by accident is not at all easy.

Interesting discussion. I'm going with the newtype approach that limits the availability of the leaky Functor instance, I think.