Triangular Matrix Type in Idris

GeneralisedDependentMatrix.idr

module GeneralisedDependentMatrix

import Data.Vect

neg : Int -> Int
neg x = -x

-- Vect (len: Nat) (elemt: Type)

-- A generalisation of the TriangularMatrix type
DependentMatrix : (n: Nat) -> (Fin n -> Nat) -> Type -> Type
DependentMatrix n f t = Vect n (m: (Fin n) ** Vect (f m) t) -- MAGICAL ORDING PROPERTY

-- Triangular ascending row length
AscendingMatrix : Nat -> Type -> Type
AscendingMatrix n t = DependentMatrix n (\m => (finToNat m) + 1) t

xs : AscendingMatrix 3 Int
xs = [ (0 ** [1]),
       (1 ** [2, 3]),
       (2 ** [4, 5, 6]) ]

xsNeg : AscendingMatrix 3 Int
xsNeg = map (\ (i ** x) => (i ** map neg x)) xs

xsSum : Vect 3 Int
xsSum = map (\ (_ ** x) => sum x) xs

-- Triangular descending row length
DescendingMatrix : Nat -> Type -> Type
DescendingMatrix n t = DependentMatrix n (\m => minus n (finToNat m)) t

ys : DescendingMatrix 3 Int
ys = [ (0 ** [1, 2, 3]),
       (1 ** [4, 5]),
       (2 ** [6]) ]

ysNeg : DescendingMatrix 3 Int
ysNeg = map (\ (_ ** y) => (_ ** map neg y)) ys

ysSum : Vect 3 Int
ysSum = map (\ (_ ** y) => sum y) ys

-- Binary Tree
BinaryTree : Nat -> Type -> Type
BinaryTree n t = DependentMatrix n (\m => power 2 (finToNat m)) t

zs : BinaryTree 3 Int
zs = [ (0 ** [     1    ]),
       (1 ** [  2,    3 ]),
       (2 ** [4, 5, 6, 7]) ]

zsNeg : BinaryTree 3 Int
zsNeg = map (\ (_ ** z) => (_ ** map neg z)) zs

zsSum : Vect 3 Int
zsSum = map (\ (_ ** z) => sum z) zs






Vect' : (n: Nat) -> (Fin n -> Type) -> Type

-- data Vect' : (n: Nat) -> (Fin n -> Type) -> Type where
--   Empty  : (elem: Type) -> Vect' Z (\_ => elem)
--   Append : (elem: Type) -> (xs: Vect' len f) -> Vect' (S len) (\i => if ((finToNat i) == len + 1) then elem else (f i) )

Triangle : (n: Nat) -> (a: Type) -> Vect' n (\i => Vect' (finToNat i) (\_ => a))

Matrix.idr

module Matrix

import Data.Vect

Matrix : Nat -> Nat -> Type -> Type
Matrix n m t = Vect n (Vect m t)

xs : Matrix 3 2 Int
xs = [ [1, 2],
       [3, 4],
       [5, 6] ]

neg : Int -> Int
neg x = -x

negMatrix : Matrix n m Int -> Matrix n m Int
negMatrix = map (map neg)

rowSumOfMatrix : Matrix n m Int -> Vect n Int
rowSumOfMatrix = map sum

xsNeg : Matrix 3 2 Int
xsNeg = negMatrix xs

xsSum : Vect 3 Int
xsSum = rowSumOfMatrix xs

Ragged.idr

module Ragged

import Data.Vect

neg : Int -> Int
neg x = -x

-- This models a ragged matrix using a vector which holds the length of each row.
-- The matrix elements are dependent pairs, where the first component is the
-- index of the row used to index into the length vector.
-- The Fin enforces that the indices into the length vector are in bound.
-- The order of the rows is not enforced by the type, e.g. it is even fine to
-- index into the same elemt multiple times.
RaggedMatrix : (n: Nat) -> Vect n Nat -> Type -> Type
RaggedMatrix n ms t = Vect n (i: (Fin n) ** Vect (Data.Vect.index i ms) t)

RowLength : Vect 3 Nat
RowLength = [2, 1, 4]

xs : RaggedMatrix 3 RowLength Int
xs = [ (0 ** [1, 2]),
       (1 ** [3]),
       (2 ** [4, 5, 6, 7]) ]

negRaggedMatrix : RaggedMatrix n ms Int -> RaggedMatrix n ms Int
negRaggedMatrix = map ( \ (_ ** x) => (_ ** map neg x) )

rowSumOfRaggedMatrix : RaggedMatrix n ms Int -> Vect n Int
rowSumOfRaggedMatrix = map (\ (_ ** x) => sum x )

xsNeg : RaggedMatrix 3 RowLength Int
xsNeg = negRaggedMatrix xs

xsSum : Vect 3 Int
xsSum = rowSumOfRaggedMatrix xs

Triangle.idr

module Triangle

import Data.Vect

neg : Int -> Int
neg x = -x

-- This models a triangular matrix using a dependent pair, where the first
-- component is an arbitrary Nat corresponding to the length of the row.
TriangularMatrix : Nat -> Type -> Type
TriangularMatrix n t = Vect n (m: Nat ** Vect m t)

-- Using this design we can leave the index blank as it is infered from the type
xs : TriangularMatrix 3 Int
xs = [ (_ ** [1]),
       (_ ** [2, 3]),
       (_ ** [4, 5, 6]) ]
{-
-- This models a triangular matrix using a dependent pair, where the first
-- component is a number smaller than n (see Data.Fin) and the length of the
-- row is then (n + 1).
TriangularMatrix : Nat -> Type -> Type
TriangularMatrix n t = Vect n (m: (Fin n) ** Vect ((finToNat m) + 1) t)

xs : TriangularMatrix 3 Int
xs = [ (0 ** [1]),
       (1 ** [2, 3]),
       (2 ** [4, 5, 6]) ]
-}

negTriangularMatrix : TriangularMatrix n Int -> TriangularMatrix n Int
negTriangularMatrix = map ( \ (_ ** x) => (_ ** map neg x) )
-- or:
{-
negTriangularMatrix = map (dmap (map neg)) where
  -- Can't get the generic version to work.
  -- This definition type checks, but it's application doesn't
  -- dmap : {a : Type} -> {P : a -> Type} ->
  --        ({b: Type} -> b -> b) -> DPair a P -> DPair a P
  dmap : ({n: Nat} -> Vect n t -> Vect n t) -> (m: Nat ** Vect m t) -> (m: Nat ** Vect m t)
  dmap f (x ** y) = (x ** (f y))
-}

rowSumOfTriangularMatrix : TriangularMatrix n Int -> Vect n Int
rowSumOfTriangularMatrix = map (\ (_ ** x) => sum x )

xsNeg : TriangularMatrix 3 Int
xsNeg = negTriangularMatrix xs

xsSum : Vect 3 Int
xsSum = rowSumOfTriangularMatrix xs