Noether.Algebra.Vector.Tutorial

A work-in-progress tutorial for Noether vectors.

This module demonstrates creating vectors, using simple operators to transform them, and techniques that leverage type system features to provide improved correctness guarantees.

Basics

Vectors are constructed with unsafeFromList, which wraps fromList under the hood.

v :: BVector 10 (Complex Double)
v = unsafeFromList $ map (\x -> cis (x * pi / 10)) [1..10]

w :: BVector 10 (Complex Double)
w = unsafeFromList $ map (\x -> cis (-x * pi / 10)) [1..10]

The type annotations actually do nothing but bring the KnownNat constraint into scope. (TODO demo with PartialTypeSignatures?)

func x = x + x - x * x + zero

The inferred type of func is somewhat hairy:

func
  :: ( CancellativeK 'Add a (CancellativeS 'Add a)
     , MagmaK 'Add a (MagmaS 'Add a)
     , MagmaK 'Mul a (MagmaS 'Mul a)
     , NeutralK 'Add a (NeutralS 'Add a)
     ) => a -> a

which is an expanded version of

func
  :: ( Cancellative 'Add a
     , Magma 'Add a
     , Magma 'Mul a
     , Neutral 'Add a
     ) => a -> a

but can be understood as asking for a type a that supports subtraction (Cancellative Add), addition (Magma Add), and multiplication (Magma Mul), and has a zero (Neutral Add).

g = map (\lambda -> lerp (lambda :+ 0) v (func w)) [0.0,0.1..1.0 :: Double]

Computing with statically differentiable but unknown dimensions, a la subhask

Given an action of a on b, a %< b computes the result. Usually, this is just multiplication. Other interesting examples exist: e.g. group actions, where b is just a set, and so on.

A particularly pervasive one is the action of Z on groups:

n %< a = a + a + ... + a

where the right side is a added to itself n times.

u1 :: BVector "a" Double
u1 = unsafeFromList [1..10]

u2 :: BVector "b" Double
u2 = unsafeFromList [1..10]

u3 :: BVector "a" Double
u3 = unsafeFromList [1..10]

s = u1 + x %< u3
  where
    x = 0.3 :: Double

This fails:

t = u1 + u2

  • Couldn't match type ‘"b"’ with ‘"a"’
    Expected type: BVector "a" Double
      Actual type: BVector "b" Double

You need to do the whole "I know what I'm doing":

t = u1 + unsafeChangeDimension u3