I'm using the linear
library, and I'm trying to create a way to reason about triangular matrices.
As a first step, I'm trying to create a way to figure out the size of a lower triangular matrix. So for example, a M22
has a lower triangular matrix with 3 elements, so it would be mapped to V3
.
Here is my attempt:
import Linear
type family LowerTriPacked v :: * -> *
type instance LowerTriPacked V0 = V0
type instance LowerTriPacked V1 = V1
type instance LowerTriPacked V2 = V3
But it doesn't type check, with:
Expecting one more argument to ‘V0’
The first argument of ‘LowerTriPacked’ should have kind ‘*’,
but ‘V0’ has kind ‘* -> *’
In the type ‘V0’
In the type instance declaration for ‘LowerTriPacked’
This does type check:
type family LowerTriPacked2 v :: *
type instance LowerTriPacked2 (V0 a) = V0 a
type instance LowerTriPacked2 (V1 a) = V1 a
type instance LowerTriPacked2 (V2 a) = V3 a
But it's not what I want, since now I can't use
class (Traversable (LowerTriPacked2 v a)) => Triangular v a
Because Traversable
has kind * -> *
.
What's wrong with my syntax for the first attempt?
The default kind for arguments is *
; but you can override the default by giving a kind annotation. Like this:
type family LowerTriPacked (v :: * -> *) :: * -> *
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With