Copyright | (c) Justus Sagemüller 2015 |
---|---|
License | GPL v3 |
Maintainer | (@) sagemueller $ geo.uni-koeln.de |
Stability | experimental |
Portability | portable |
Safe Haskell | None |
Language | Haskell2010 |
This is the second prototype of a manifold class. It appears to give considerable
advantages over Manifold
, so that class will probably soon be replaced
with the one we define here (though PseudoAffine
does not follow the standard notion
of a manifold very closely, it should work quite equivalently for pretty much all
Haskell types that qualify as manifolds).
Manifolds are interesting as objects of various categories, from continuous to diffeomorphic. At the moment, we mainly focus on region-wise differentiable functions, which are a promising compromise between flexibility of definition and provability of analytic properties. In particular, they are well-suited for visualisation purposes.
- class PseudoAffine x where
- type PseudoDiff x :: *
- (.-~.) :: x -> x -> Option (PseudoDiff x)
- (.+~^) :: x -> PseudoDiff x -> x
- data Region s m
- data Differentiable s d c
- data PWDiffable s d c
- data RWDiffable s d c
Manifold class
class PseudoAffine x where Source
PseudoAffine
is intended as an alternative class for Manifold
s.
The interface is almost identical to the better-known AffineSpace
class, but unlike
in the mathematical definition of affine spaces we don't require associativity
of .+~^
with ^+^
– except in an asymptotic sense for small vectors.
That innocent-looking change makes the class applicable to vastly more general types: while an affine space is basically nothing but a vector space without particularly designated origin, a pseudo-affine space can have nontrivial topology on the global scale, and yet be used in practically the same way as an affine space. At least the usual spheres and tori make good instances, perhaps the class is in fact equivalent to parallelisable manifolds.
type PseudoDiff x :: * Source
(.-~.) :: x -> x -> Option (PseudoDiff x) infix 6 Source
(.+~^) :: x -> PseudoDiff x -> x infixl 6 Source
PseudoAffine Double | |
PseudoAffine Rational | |
PseudoAffine S² | |
PseudoAffine S¹ | |
PseudoAffine (ZeroDim k) | |
(PseudoAffine a, PseudoAffine b) => PseudoAffine (a, b) | |
(PseudoAffine a, PseudoAffine b, PseudoAffine c) => PseudoAffine (a, b, c) |
Regions within a manifold
A pathwise connected subset of a manifold m
, whose tangent space has scalar s
.
Hierarchy of manifold-categories
data Differentiable s d c Source
The category of differentiable functions between manifolds over scalar s
.
As you might guess, these offer automatic differentiation of sorts (basically, simple forward AD), but that's in itself is not really the killer feature here. More interestingly, we actually have the (à la Curry-Howard) proof built in: the function f has at x₀ derivative f'ₓ₀, if, for¹ ε>0, there exists δ such that |f x − (f x₀ + x⋅f'ₓ₀)| < ε for all |x − x₀| < δ.
Observe that, though this looks quite similar to the standard definition of differentiability, it is not equivalent thereto – in fact it does not prove any analytic properties at all. To make it equivalent, we need a lower bound on δ: simply δ gives us continuity, and for continuous differentiability, δ must grow at least like √ε for small ε. Neither of these conditions are enforced by the type system, but we do require them for any allowed values because these proofs are obviously tremendously useful – for instance, you can have a root-finding algorithm and actually be sure you get all solutions correctly, not just some that are (hopefully) the closest to some reference point you'd need to laborously define!
Unfortunately however, this also prevents doing any serious algebra etc. with the
category, because even something as simple as division necessary introduces singularities
where the derivatives must diverge.
Not to speak of many trigonometric e.g. trigonometric functions that
are undefined on whole regions. The PWDiffable
and RWDiffable
categories have explicit
handling for those issues built in; you may simply use these categories even when
you know the result will be smooth in your relevant domain (or must be, for e.g.
physics reasons).
¹(The implementation does not deal with ε and δ as difference-bounding reals, but rather as metric tensors that define a boundary by prohibiting the overlap from exceeding one; this makes the concept actually work on general manifolds.)
VectorSpace s => Morphism (Differentiable s) | |
VectorSpace s => PreArrow (Differentiable s) | |
VectorSpace s => WellPointed (Differentiable s) | |
VectorSpace s => CartesianAgent (Differentiable s) | |
VectorSpace s => Category (Differentiable s) | |
VectorSpace s => Cartesian (Differentiable s) | |
VectorSpace s => HasAgent (Differentiable s) | |
RealDimension s => EnhancedCat (RWDiffable s) (Differentiable s) | |
RealDimension s => EnhancedCat (PWDiffable s) (Differentiable s) | |
type UnitObject (Differentiable s) = ZeroDim s | |
type PointObject (Differentiable s) x = () | |
type Object (Differentiable s) o | |
type PairObjects (Differentiable s) a b = () | |
type AgentVal (Differentiable s) a v = GenericAgent (Differentiable s) a v |
data PWDiffable s d c Source
Category of functions that almost everywhere have an open region in which they are continuously differentiable, i.e. PieceWiseDiff'able.
RealDimension s => Morphism (PWDiffable s) | |
RealDimension s => PreArrow (PWDiffable s) | |
RealDimension s => WellPointed (PWDiffable s) | |
RealDimension s => CartesianAgent (PWDiffable s) | |
RealDimension s => Category (PWDiffable s) | |
RealDimension s => Cartesian (PWDiffable s) | |
RealDimension s => HasAgent (PWDiffable s) | |
RealDimension s => EnhancedCat (RWDiffable s) (PWDiffable s) | |
RealDimension s => EnhancedCat (PWDiffable s) (Differentiable s) | |
type UnitObject (PWDiffable s) = ZeroDim s | |
type PointObject (PWDiffable s) x = () | |
type Object (PWDiffable s) o | |
type PairObjects (PWDiffable s) a b = () | |
type AgentVal (PWDiffable s) a v = GenericAgent (PWDiffable s) a v |
data RWDiffable s d c Source
Category of functions that, where defined, have an open region in
which they are continuously differentiable. Hence RegionWiseDiff'able.
Basically these are the partial version of PWDiffable
.
Though the possibility of undefined regions is of course not too nice
(we don't need Java to demonstrate this with its everywhere-looming null
values...),
this category will propably be the “workhorse” for most serious
calculus applications, because it contains all the usual trig etc. functions
and of course everything algebraic you can do in the reals.
The easiest way to define ordinary functions in this category is hence
with its AgentVal
ues, which have instances of the standard classes Num
through Floating
. For instance, the following defines the binary entropy
as a differentiable function on the interval ]0,1[
: (it will
actually know where it's defined and where not! – and I don't mean you
need to exhaustively isNaN
-check all results...)
hb :: RWDiffable R R R hb = alg (\p -> - p * logBase 2 p - (1-p) * logBase 2 (1-p) )
RealDimension s => Morphism (RWDiffable s) | |
RealDimension s => PreArrow (RWDiffable s) | |
RealDimension s => WellPointed (RWDiffable s) | |
RealDimension s => CartesianAgent (RWDiffable s) | |
RealDimension s => Category (RWDiffable s) | |
RealDimension s => Cartesian (RWDiffable s) | |
RealDimension s => HasAgent (RWDiffable s) | |
RealDimension s => EnhancedCat (RWDiffable s) (PWDiffable s) | |
RealDimension s => EnhancedCat (RWDiffable s) (Differentiable s) | |
type UnitObject (RWDiffable s) = ZeroDim s | |
type PointObject (RWDiffable s) x = () | |
type Object (RWDiffable s) o | |
type PairObjects (RWDiffable s) a b = () | |
type AgentVal (RWDiffable s) a v = GenericAgent (RWDiffable s) a v |