Data.SimplicialComplex

Simplices

data Simplex :: Nat -> * -> * where

An n-simplex is a connection of n+1 points in a simply connected region of a manifold.

Constructors

ZS :: !x -> Simplex Z x

(:<|) :: KnownNat n => !x -> !(Simplex n x) -> Simplex (S n) x infixr 5

Instances

Functor (Simplex n)

Show x => Show (Simplex n x)

Construction

(.<.) :: x -> x -> Simplex One x infixr 5

Use this together with :<| to easily build simplices, like you might construct lists. E.g. (0,0) :<| (1,0) .<. (0,1) :: Simplex Two ℝ².

makeSimplex :: forall x n. KnownNat n => (x ^ S n) -> Simplex n x

makeSimplex' :: forall x n. KnownNat n => [x] -> Option (Simplex n x)

Deconstruction

simplexVertices :: forall x n. Simplex n x -> x ^ S n

simplexVertices' :: forall x n. Simplex n x -> [x]

Simplicial complexes

data Triangulation n x

An n-dimensional abstract simplicial complex is a collection of n-simplices which are “glued together” in some way. The preferred way to construct such complexes is to run a TriangT builder.

Instances

Functor (Triangulation n)

Show x => Show (Triangulation n x)

KnownNat n => Monoid (Triangulation n x)

KnownNat n => Semigroup (Triangulation n x)

Combine two triangulations (assumed as disjoint) to a single, non-connected complex.

singleSimplex :: forall n x. KnownNat n => Simplex n x -> Triangulation n x

Consider a single simplex as a simplicial complex, consisting only of this simplex and its faces.

Triangulation-builder monad

data TriangT t n x m y

A “conservative” state monad containing a Triangulation. It can be extended by new simplices, which can then be indexed using SimplexIT. The universally-quantified t argument ensures you can't index simplices that don't actually exist in this triangulation.

Instances

MonadTrans (TriangT t n x)

(Functor m, Monad m (->)) => Monad (TriangT t n x m)

Functor m => Functor (TriangT t n x m)

(Functor m, Monad m (->)) => Applicative (TriangT t n x m)

evalTriangT :: forall n x m y. (KnownNat n, HaskMonad m) => (forall t. TriangT t n x m y) -> m y

runTriangT :: forall n x m y. (forall t. TriangT t n x m y) -> Triangulation n x -> m (y, Triangulation n x)

doTriangT :: forall n x m y. KnownNat n => (forall t. TriangT t n x m y) -> m (y, Triangulation n x)

getTriang :: forall t n k x m. (HaskMonad m, KnownNat k, KnownNat n) => TriangT t n x m (Option (Triangulation k x))

Subsimplex-references

data SimplexIT t n x

Instances

Eq (SimplexIT t n x)

Ord (SimplexIT t n x)

Show (SimplexIT t n x)

simplexITList :: forall t m n k x. (HaskMonad m, KnownNat k, KnownNat n) => TriangT t n x m [SimplexIT t k x]

lookSimplex :: forall t m n k x. (HaskMonad m, KnownNat k, KnownNat n) => SimplexIT t k x -> TriangT t n x m (Simplex k x)

lookSplxFacesIT :: forall t m n k x. (HaskMonad m, KnownNat k, KnownNat n) => SimplexIT t (S k) x -> TriangT t n x m (SimplexIT t k x ^ S (S k))

Reference the k-faces of a given simplex in a triangulation.

lookSupersimplicesIT :: forall t m n k j x. (HaskMonad m, KnownNat k, KnownNat j, KnownNat n) => SimplexIT t k x -> TriangT t n x m [SimplexIT t j x]

tgetSimplexIT :: SimplexIT t n x -> Int

A unique (for the given dimension) ID of a triagulation's simplex. It is the index where that simplex can be found in the simplexITList.

lookVertexIT :: forall t m n x. (HaskMonad m, KnownNat n) => SimplexIT t Z x -> TriangT t n x m x

lookSplxVerticesIT :: forall t m n k x. (HaskMonad m, KnownNat k, KnownNat n) => SimplexIT t k x -> TriangT t n x m (SimplexIT t Z x ^ S k)

sharedBoundary :: forall t m n k x. (HaskMonad m, KnownNat k, KnownNat n) => SimplexIT t (S k) x -> SimplexIT t (S k) x -> TriangT t n x m (Option (SimplexIT t k x))

distinctSimplices :: forall t m n k x. (HaskMonad m, KnownNat k, KnownNat n) => SimplexIT t (S k) x -> SimplexIT t (S k) x -> TriangT t n x m (Option (NeighbouringSimplices t k x))

type NeighbouringSimplices t n x = ((SimplexIT t Z x, SimplexIT t Z x), SimplexIT t n x)

Building triangulations

disjointTriangulation :: forall t m n x. (KnownNat n, HaskMonad m) => Triangulation n x -> TriangT t n x m [SimplexIT t n x]

Import an entire triangulation, as disjoint from everything already in the monad.

disjointSimplex :: forall t m n x. (KnownNat n, HaskMonad m) => Simplex n x -> TriangT t n x m (SimplexIT t n x)

mixinTriangulation :: forall t m f k n x. (KnownNat n, KnownNat k, HaskMonad m, Functor f (->) (->)) => (forall s. TriangT s n x m (f (SimplexIT s k x))) -> TriangT t n x m (f (SimplexIT t k x))

Import a triangulation like with disjointTriangulation, together with references to some of its subsimplices.

introVertToTriang :: forall t m n x. (HaskMonad m, KnownNat n) => x -> [SimplexIT t n x] -> TriangT t (S n) x m (SimplexIT t Z x)

webinateTriang :: forall t m n x. (HaskMonad m, KnownNat n) => SimplexIT t Z x -> SimplexIT t n x -> TriangT t (S n) x m (SimplexIT t (S n) x)

Misc util

type HaskMonad m = (Applicative m, Monad m)

liftInTriangT :: forall t n x m μ y. (HaskMonad m, MonadTrans μ) => TriangT t n x m y -> TriangT t n x (μ m) y

unliftInTriangT :: forall t n x m μ y. (HaskMonad m, MonadTrans μ) => (forall m' a. μ m a -> m a) -> TriangT t n x (μ m) y -> TriangT t n x m y

data Nat

Mainly intended to be used as a data kind. Of course, we'd rather use GHC.TypeLits naturals, but they aren't mature enough yet.

Instances

Eq Nat

type Zero = Z

Type-level zero of kind Nat.

type One = S Zero

type Two = S One

type Three = S Two

type Succ = S