Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Type instance that returns * -> *

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?

like image 369
yong Avatar asked Dec 20 '22 07:12

yong


1 Answers

The default kind for arguments is *; but you can override the default by giving a kind annotation. Like this:

type family LowerTriPacked (v :: * -> *) :: * -> *
like image 111
Daniel Wagner Avatar answered Jan 14 '23 05:01

Daniel Wagner