More general type for ident

[dmcclean]

Right now we have

ident :: forall ones a _1.
    (H.Field a, HNat2Integral (HLength ones), ones ~ (DOne ': _1)) =>
    DimMat [ones, ones] a
ident = DimMat (H.ident (hNat2Integral (proxy :: Proxy (HLength ones))))

I'm not convinced that this is the most general type. For a while I thought it was at least the most general we would need, but then I got to implementing this example. I can't bookmark the specific line, but scroll down a bit to where there is an expression defining Bd.

For convenience I will hotlink the latex image:

In this case, Ad has dimensions taking the discrete-time state vector to itself. As a result, the dimensions are all DOne along the main diagonal, but the ones that are off the main diagonal in general have other dimensions.

For the running pendulum example, picking a discrete time step of 0.01 *~ second, Ad is:

4><4	1	s	m	m s
1	1.0	9.990914092164536e-3	1.3359012218891594e-4	4.453215697426472e-7
s^-1	0.0	0.9981832677461657	2.6716874509823567e-2	1.3359012218891594e-4
m^-1	0.0	-2.271940853552991e-5	1.0015592936281539	1.0005197273892413e-2
m^-1 s^-1	0.0	-4.543686141126454e-3	0.311919519484923	1.0015592936281539

Note that the row dimensions are the reciprocal of the column dimensions, and that the (1,1) dimension (and thus all the main diagonal dimensions) are DOne. It also happens that they are all very close to 1, which makes sense because we want each time step to only involve a small movement in the state space.

To evaluate the expression Ad - I, we can either relax the type of ident to allow it to match the type of Ad, or we can invent another name for this more general ident.

[dmcclean]

See this commit for the solution where we relax the type. It works, just not sure if it is a good idea.